chore: remove temporary reviewdog fix (#12284)

- [x] depends on: reviewdog/action-suggester#52 This reverts #12280 after the upstream fix reviewdog/reviewdog#1696 has propagated to reviewdog/action-suggester@v1. This should happen when https://github.com/reviewdog/action-suggester/releases has a release that uses [v0.17.4](https://github.com/reviewdog/reviewdog/releases/tag/v0.17.4) or higher. When this happens, rebase this pull request and re-trigger to see that it doesn't fail with the 300 dummy files. Then remove the dummy files and merge this pull request. Co-authored-by: Moritz Firsching <[email protected]>
leanprover-community · May 16, 2024 · 818c378 · 818c378
1 parent 89769e1
commit 818c378
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml
@@ -27,8 +27,6 @@ jobs:
           ./scripts/lint-style.sh --fix
 
       - name: suggester / lint-style
-        # temporary fix for https://github.com/reviewdog/reviewdog/issues/1696#issue-2206596164
-        if: ${{ github.event.pull_request.changed_files < 301 }}
         uses: reviewdog/action-suggester@v1
         with:
           tool_name: lint-style
@@ -44,8 +42,6 @@ jobs:
           ./scripts/lint-bib.sh
 
       - name: suggester / lint-bib
-        # temporary fix for https://github.com/reviewdog/reviewdog/issues/1696#issue-2206596164
-        if: ${{ github.event.pull_request.changed_files < 301 }}
         uses: reviewdog/action-suggester@v1
         with:
           tool_name: lint-bib
@@ -78,8 +74,6 @@ jobs:
           git ls-files 'Archive/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Archive.lean
 
       - name: suggester / import list
-        # temporary fix for https://github.com/reviewdog/reviewdog/issues/1696#issue-2206596164
-        if: ${{ github.event.pull_request.changed_files < 301 }}
         uses: reviewdog/action-suggester@v1
         with:
           tool_name: imports