summaryrefslogtreecommitdiff
path: root/tests/lean/lakefile.lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/lakefile.lean1
1 files changed, 0 insertions, 1 deletions
diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean
index 3a777824..bb13ddf2 100644
--- a/tests/lean/lakefile.lean
+++ b/tests/lean/lakefile.lean
@@ -13,7 +13,6 @@ package «tests» {}
@[default_target] lean_lib Constants
@[default_target] lean_lib External
@[default_target] lean_lib Hashmap
-@[default_target] lean_lib HashmapMain
@[default_target] lean_lib Loops
@[default_target] lean_lib NoNestedBorrows
@[default_target] lean_lib Paper