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 5, 2024 · 4218856 · 4218856
1 parent ff35083
commit 4218856
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