fix(nolints.yml): correct the main step of the update-nolints wor…

…kflow (#13343)

This fixes the main step of the `update_nolints` workflow.
As I see it, this was quite impressive: about three bugs in four lines of code.
- updating `nolints.json` now works using the `update` option: no need to run the linter and move some file (presumably, that file wouldn't exist either)
- running `git diff` right after generating the exceptions didn't work: no git repository was configured yet
- wrapping things in `problem-matcher-wrap` was a bad idea, as that only supports one command: instead, we remove the matcher, as we don't need this here

Since this workflow was originally cargo-culted from the mathlib one, I view this also as a cautionary tale about cargo cult programming.

.github/workflows/nolints.yml

@@ -53,16 +53,11 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-      - name: lint mathlib
-        id: lint
-        uses: liskin/gh-problem-matcher-wrap@v2
-        with:
-          linters: gcc
-          run: |
-            env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib
-            mv nolints.json scripts/nolints.json
-            ./scripts/update-style-exceptions.sh
-            git diff
+      - name: update nolints.json and style-exceptions.txt
+        shell: bash
+        run: |
+          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --update Mathlib
+          ./scripts/update-style-exceptions.sh
 
       - name: configure git setup
         run: |
@@ -75,7 +70,7 @@ jobs:
           # github using a different username.
           git config --unset http.https://github.com/.extraheader
 
-      - name: update nolints.json and style-exceptions.txt
+      - name: file a new PR to update nolints.json and style-exceptions.txt
         run: ./scripts/update_nolints_CI.sh
         env:
           DEPLOY_GITHUB_TOKEN: ${{ secrets.UPDATE_NOLINTS_TOKEN }}