Update: ignore nothing to commit

release-docs.sh

@@ -25,5 +25,5 @@ cp -r $SOURCE_DIR/docs/_site/* .
 
 echo "Push the new docs to the remote branch"
 git add . -A
-git commit -m "Update generated documentation"
+git diff-index --quiet HEAD || git commit -m "Update generated documentation"
 git push origin master