Updated release script

Author: Nathan Speidel

bin/release.sh

@@ -1,7 +1,9 @@
 #!/bin/sh
 
-# This script will build the documentation from the current "src" branch and push it to the "master" branch.
-# "mkdocs" must be available, and you must be in a clean git environment ("git diff" should print nothing).
+# This script will build the documentation from the current "src" branch. "mkdocs" must be available, and
+# you must be in a clean git environment ("git diff" should print nothing). The java-docs folder in the
+# master branch will not be replaced with the corresponding folder build from the src branch, which is just
+# a placeholder.
 
 git checkout src
 git pull
@@ -22,9 +24,13 @@ mv site/ /tmp/tmp-folder-for-bullet-docs/
 echo Checking out master...
 git checkout master
 git pull
-# Carefully delete everything in this folder
+# Save the JavaDocs currently in master branch
+mv java-docs/ /tmp/tmp-folder-for-bullet-docs/
 rm -rf ./*
 cp -r /tmp/tmp-folder-for-bullet-docs/site/ ./
+# Delete fake java-docs and replace with saved ones
+rm -rf ./java-docs/
+mv /tmp/tmp-folder-for-bullet-docs/java-docs/ ./
 rm -rf /tmp/tmp-folder-for-bullet-docs/
 git add -A
 git commit -m "Build at ${COMMIT}"