Skip to content

Commit

Permalink
remove references to old action files
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed Jan 16, 2025
1 parent be63871 commit dda9d8e
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions .github/workflows/lint_and_suggest_pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ jobs:
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
# if you update this step (or its dependencies), please also update them in bot_fix_style_comment.yaml
# if you update this step (or its dependencies), please also update them in bot_fix_style.yaml
- name: lint
run: |
lake exe lint-style --fix
Expand All @@ -43,7 +43,7 @@ jobs:
sudo apt-get update
sudo apt-get install -y bibtool
# if you update this step (or its dependencies), please also update them in bot_fix_style_comment.yaml
# if you update this step (or its dependencies), please also update them in bot_fix_style.yaml
- name: lint references.bib
run: |
# ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
Expand Down Expand Up @@ -72,9 +72,9 @@ jobs:
./elan-init -y --default-toolchain none
echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
# if you update this step (or its dependencies), please also update them in bot_fix_style_comment.yaml
# if you update this step (or its dependencies), please also update them in bot_fix_style.yaml
- name: update {Mathlib, Tactic, Counterexamples, Archive}.lean
run:
run:
# ignoring the return code allows the following `reviewdog` step to add GitHub suggestions
lake exe mk_all || true

Expand Down

0 comments on commit dda9d8e

Please sign in to comment.