Merge remote-tracking branch 'origin/master' into PR_test

RemyDegenne · Dec 28, 2023 · bfb095f · bfb095f
2 parents 08c92f5 + a1bdad6
commit bfb095f
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/.github/workflows/push_pr.yml b/.github/workflows/push_pr.yml
@@ -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
@@ -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