chore: switch to lakefile.toml (#1005)

leanprover-community · Oct 22, 2024 · dc72dcd · dc72dcd
1 parent 7c5548e
commit dc72dcd
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 18 deletions.
diff --git a/lakefile.lean b/lakefile.lean
diff --git a/lakefile.toml b/lakefile.toml
@@ -0,0 +1,19 @@
+name = "batteries"
+testDriver = "test"
+lintDriver = "runLinter"
+defaultTargets = ["Batteries", "runLinter"]
+
+[leanOptions]
+linter.missingDocs = true
+
+[[lean_lib]]
+name = "Batteries"
+
+[[lean_exe]]
+name = "runLinter"
+srcDir = "scripts"
+supportInterpreter = true
+
+[[lean_exe]]
+name = "test"
+srcDir = "scripts"