Skip to content

Commit

Permalink
PFR -> Clt in push_pr.yml
Browse files Browse the repository at this point in the history
  • Loading branch information
RemyDegenne committed Dec 28, 2023
1 parent faa9014 commit a1bdad6
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions .github/workflows/push_pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,12 @@ jobs:
- name: Check for long lines
if: always()
run: |
! (find PFR -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
! (find Clt -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
- name: Don't 'import Mathlib', use precise imports
if: always()
run: |
! (find PFR -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
! (find Clt -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
build_project:
runs-on: ubuntu-latest
Expand All @@ -35,4 +35,4 @@ jobs:
run: ~/.elan/bin/lake exe cache get || true

- name: Build project
run: ~/.elan/bin/lake build PFR
run: ~/.elan/bin/lake build Clt

0 comments on commit a1bdad6

Please sign in to comment.