chore: update make lint to use lake (#791)

* chore: update make lint to use lake * Update GNUmakefile Co-authored-by: Mac Malone <tydeu@hatpress.net> --------- Co-authored-by: Mac Malone <tydeu@hatpress.net>
leanprover-community · May 13, 2024 · dd6e639 · dd6e639
1 parent cac5bff
commit dd6e639
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/GNUmakefile b/GNUmakefile
@@ -18,5 +18,5 @@ test: $(TESTS)
 %.run: build
 	lake env lean $(@:.run=.lean)
 
-lint: build
-	./.lake/build/bin/runLinter
+lint:
+	lake exe runLinter