Rework publication script (no longer erase TIP first)

tools/travis-publish-spec.sh

@@ -1,20 +1,29 @@
 #!/bin/bash
 
-if [ "$TRAVIS_REPO_SLUG" == "$GIT_PUB_REPO" ]; then
-    echo -e "Setting up for publication...\n"
+if [ "$TRAVIS_PULL_REQUEST" != "false" ]; then
+    echo "Cannot publish pull requests."
+    exit
+fi
 
+if [ "$TRAVIS_REPO_SLUG" == "$GIT_PUB_REPO" ]; then
+    echo "Preparing to publish..."
     cd $HOME
     git config --global user.email ${GIT_EMAIL}
     git config --global user.name ${GIT_NAME}
-    git clone --quiet --branch=gh-pages https://${GH_TOKEN}@github.com/${GIT_PUB_REPO} gh-pages > /dev/null
 
-    if [ "$TRAVIS_PULL_REQUEST" == "false" ]; then
-        echo -e "Publishing specification...\n"
+    if [ "$GH_TOKEN" != "" ]; then
+        echo "Publishing..."
+
+        git clone --quiet --branch=gh-pages \
+            https://${GH_TOKEN}@github.com/${GIT_PUB_REPO} gh-pages > /dev/null
 
         TIP=${TRAVIS_TAG:="head"}
 
+        # N.B. gh-pages here is updated by two different repositories.
+        # Consequently, we don't try to remove the old files.
+        # Occasional manual cleanup may be required.
+
         cd gh-pages
-        git rm -rf ./${TRAVIS_BRANCH}/${TIP} > /dev/null
         mkdir -p ./${TRAVIS_BRANCH}/${TIP}
         cp -Rf $TRAVIS_BUILD_DIR/build/dist/* ./${TRAVIS_BRANCH}/${TIP}