diff --git a/website/dummy.txt b/website/dummy.txt deleted file mode 100644 index 6cd25eecc..000000000 --- a/website/dummy.txt +++ /dev/null @@ -1,4 +0,0 @@ -This file doesn't do anything, but we periodically update the number -below just to force being able to deploy the website again. - -1 diff --git a/website/version.txt b/website/version.txt deleted file mode 100644 index 0d4adf742..000000000 --- a/website/version.txt +++ /dev/null @@ -1,3 +0,0 @@ -Just increment this number if you have to deploy the website: - -3