Don't create new gh-pages commit if there are no documentation changes

[christophebedard]

Even if there are no changes, there's always a new commit since gen_docs injects the current date+time: ced6ed0

So just don't create a new commit if the "generated on ..." line in api/index.html is the only line that changed.

[christophebedard]

On second thought, whatever. I stopped trying to get this to work:

diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml
index af5de02..4e2b94f 100644
--- a/.github/workflows/doc.yml
+++ b/.github/workflows/doc.yml
@@ -53,11 +53,12 @@ jobs:
         mv -T output/master/ gh-pages/api/
         rm -rf gh-pages/design/
         mv -T pandoc/ gh-pages/design/
-    - name: Commit and push to gh-pages branch
+    - name: Commit and push to gh-pages branch if needed
       run: |
         cd gh-pages
         git config --global user.email "3717345+christophebedard@users.noreply.github.com"
         git config --global user.name "Christophe Bedard [bot]"
         git add .
-        git commit -m "Update docs"
-        git push origin gh-pages
+        number_of_new_or_modified_files=$(git status | grep -E 'modified:|new file:' | wc -l)
+        grep_ret_constant_change=$((git diff --staged | grep '+      <small><i>generated on '); echo $?)
+        if [ "$number_of_new_or_modified_files" -eq 1 ] && [ "$grep_ret_constant_change" -eq 0 ]; then echo "nothing changed"; else echo "changes, pushing" && git commit -m "Update docs" && git push origin gh-pages; fi