Add new documenation files

- skip commit if nothing to commit

Author: mrbean-bremen

.github/workflows/builddocs.yml

@@ -47,5 +47,10 @@ jobs:
           cd doc
           git config user.name "Travis CI"
           git config user.email "[email protected]"
+          git add dev/*
+          if [ `git status -s | wc -l` = 0 ]; then
+            echo "No changes in built documentation, skipping"
+            exit 0
+          fi
           git commit -a -m "$LAST_COMMIT"
           git push