Do not make empty commits

Author: Matthias Koeppe

.ci/merge-fixes.sh

@@ -21,8 +21,11 @@ else
         git checkout -q test_head
         if git merge --no-edit --squash -q pr-$a; then
             echo "::endgroup::"
-            git commit -q -m "Merge https://github.com/$REPO/pull/$a" -a --allow-empty
-            echo "Merged #$a"
+            if git commit -q -m "Merge https://github.com/$REPO/pull/$a" -a --no-allow-empty; then
+                echo "Merged #$a"
+            else
+                echo "Empty, skipped"
+            fi
         else
             echo "::endgroup::"
             echo "Failure merging #$a, resetting"

.github/workflows/build.yml

@@ -99,9 +99,7 @@ jobs:
         # After applying the fixes, make sure all changes are marked as uncommitted changes.
         run: |
           if [ -r upstream/ci_fixes.patch ]; then
-            (cd worktree-image && git commit --quiet -m "current changes" --allow-empty -a && git am) < upstream/ci_fixes.patch
-            git reset --quiet old
-            git add --quiet -N .
+            (cd worktree-image && git commit -q -m "current changes" --allow-empty -a && git am; git reset --quiet old; git add -N .) < upstream/ci_fixes.patch
           fi
 
       - name: Incremental build, test changed files (sage -t --new)

.github/workflows/doc-build.yml

@@ -85,9 +85,7 @@ jobs:
         # After applying the fixes, make sure all changes are marked as uncommitted changes.
         run: |
           if [ -r upstream/ci_fixes.patch ]; then
-            (cd worktree-image && git commit -m "current changes" --allow-empty -a && git am) < upstream/ci_fixes.patch
-            git reset --quiet old
-            git add -N .
+            (cd worktree-image && git commit -q -m "current changes" --allow-empty -a && git am; git reset --quiet old; git add -N .) < upstream/ci_fixes.patch
           fi
 
       - name: Incremental build