Add better error handling to format-pr workflow (#1918)

It will now leave a comment when it hits a known failure case

.github/workflows/format-pr.yml

@@ -87,13 +87,16 @@ jobs:
   comment-push:
     runs-on: ubuntu-latest
     needs: comment-format-untrusted
+    permissions:
+      # Needed for the temporary token to have permission to leave comments.
+      pull-requests: write
     steps:
       - name: Checkout upstream
         uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
         with:
           repository: TurboWarp/extensions
           # Can't use the default workflow token because commits made by it won't cause more
-          # workflows to un, so any commits it pushes get stuck in limbo waiting for workflows
+          # workflows to run, so any commits it pushes get stuck in limbo waiting for workflows
           # to run that will never run.
           # Can't use a deploy key because it won't be able to access the fork that the pull
           # request is coming from.
@@ -113,15 +116,32 @@ jobs:
         with:
           name: comment-format-untrusted-artifact
           path: extensions
-      - name: Commit
+      - name: Commit and push
         run: |
+          # It wouldn't be hard to include the branch name in the comments, but that is untrusted input so it
+          # doesn't seem like a good idea to let anyone get the bot to say anything they want.
+
+          commit_failed() {
+            echo "No changes to commit"
+            gh pr comment "$PR_NUM" -b "The formatting bot didn't find any formatting issues. It currently only checks the extensions folder. To format all files, the pull request's author can manually run the 'Format pull request' workflow from the 'Actions' tab on the fork."
+            exit 0
+          }
+
+          push_failed() {
+            echo "Failed to push"
+            gh pr comment "$PR_NUM" -b "The formatting bot couldn't push changes. Either maintainer edit permission is disabled or the pull request is from a non-personal account. The pull request's author can still run the 'Format pull request' workflow from the 'Actions' tab on the fork."
+            exit 0
+          }
+
           git config --global user.name "$GITHUB_ACTOR"
           git config --global user.email "[email protected]"
           git stage .
-          git commit --author "DangoCat[bot] <[email protected]>" -m "[Automated] Format code" || echo "No changes to commit"
-      - name: Push
-        # Explicitly set push.default to upstream, otherwise by default git might complain about us being on a
-        # branch called "DangoCat/master" but the corresponding branch on remote "DangoCat" is just "master".
-        run: |
+          git commit --author "DangoCat[bot] <[email protected]>" -m "[Automated] Format code" || commit_failed
+
+          # Explicitly set push.default to upstream, otherwise by default git might complain about us being on a
+          # branch called "DangoCat/master" but the corresponding branch on remote "DangoCat" is just "master".
           git config --global push.default upstream
-          git push
+          git push || push_failed
+        env:
+          PR_NUM: "${{ github.event.issue.number }}"
+          GH_TOKEN: "${{ github.token }}"