Update build-website.sh

Author: Varun-Dutta

tools/scripts/build-website.sh

@@ -2,25 +2,25 @@
 
 set -ex
 
-VERSION_NUMBER=$1
+# VERSION_NUMBER=$1
 if [[ "$VERSION_NUMBER" == "" ]]; then
-  VERSION_NUMBER=master
+  VERSION_NUMBER=40.0
 fi
 
-BASE_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+#BASE_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
 
-echo "Updating online runner ..."
-python3 "$BASE_DIR/add_online_runner.py"
+#echo "Updating online runner ..."
+#python3 "$BASE_DIR/add_online_runner.py"
 
 # Configure Git User, mike will create gh-pages branch
 git config user.name "nobody"
 git config user.email "nobody@localhost"
 
-echo "Building docs for $VERSION_NUMBER"
-mike deploy "$VERSION_NUMBER" -F docs/mkdocs.yml -b gh-pages
+#echo "Building docs for $VERSION_NUMBER"
+#mike deploy "$VERSION_NUMBER" -F docs/mkdocs.yml -b gh-pages
 
 git checkout gh-pages
 
 #Update versions.json file
-aws s3 cp versions.json s3://updated-documentation-website/website/ .
+aws s3 cp s3://updated-documentation-website/website/versions.json . 
 jq --arg v "$VERSION_NUMBER" '([{"version": $v, "title": $v, "aliases": []}] + .)' versions.json > temp.json && mv temp.json versions.json