chore: bump lean-action to v1 (#904)

leanprover-community · Aug 5, 2024 · dc167d2 · dc167d2
1 parent 021e272
commit dc167d2
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -18,10 +18,9 @@ jobs:
 
       - id: lean-action
         name: build, test, and lint batteries
-        uses: leanprover/lean-action@v1-beta
+        uses: leanprover/lean-action@v1
         with:
           build-args: '-Kwerror'
-          lint-module: 'Batteries'
 
       - name: Check that all files are imported
         run: lake env lean scripts/check_imports.lean

diff --git a/lakefile.lean b/lakefile.lean
@@ -13,7 +13,7 @@ package batteries where
 @[default_target]
 lean_lib Batteries
 
-@[default_target]
+@[default_target, lint_driver]
 lean_exe runLinter where
   srcDir := "scripts"
   supportInterpreter := true