Merge commit '1480cea393' into clippyup

2023-01-27 21:09:08 +01:00 · 2023-01-27 21:09:08 +01:00 · 1dd773175a
commit 1dd773175a
parent 7919ef0ec5 1480cea393
57 changed files with 2262 additions and 304 deletions
--- a/src/tools/clippy/.github/workflows/clippy_bors.yml
+++ b/src/tools/clippy/.github/workflows/clippy_bors.yml
@ -157,6 +157,11 @@ jobs:
    - name: Test metadata collection
      run: cargo collect-metadata

+    - name: Test lint_configuration.md is up-to-date
+      run: |
+        echo "run \`cargo collect-metadata\` if this fails"
+        git update-index --refresh
+
  integration_build:
    needs: changelog
    runs-on: ubuntu-latest