Fix publish docs (#742)

* `git commit` must always succeed

* Add comment

.gitlab-ci.yml

@@ -327,7 +327,12 @@ publish-docs:
     # Upload files
     - git add --all --force
     - git status
-    - git commit -m "Updated docs for ${CI_COMMIT_REF_NAME} and pushed to gh-pages"
+    # `git commit` has an exit code of > 0 if there is nothing to commit.
+    # This unfortunately causes GitLab to exit immediately and mark this
+    # job as failed subsequently.
+    # We don't want to mark the entire job as failed if there's nothing to
+    # publish though, hence the `|| true`.
+    - git commit -m "Updated docs for ${CI_COMMIT_REF_NAME} and pushed to gh-pages" || true
     - git push origin gh-pages --force
   after_script:
     - rm -rf .git/ ./*