summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/hashmap_on_disk/lakefile.lean10
1 files changed, 3 insertions, 7 deletions
diff --git a/tests/lean/hashmap_on_disk/lakefile.lean b/tests/lean/hashmap_on_disk/lakefile.lean
index 0ca1ef9b..bdb614cd 100644
--- a/tests/lean/hashmap_on_disk/lakefile.lean
+++ b/tests/lean/hashmap_on_disk/lakefile.lean
@@ -4,19 +4,15 @@ open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
-package «hashmap» {
+package «hashmap_main» {
-- add package configuration options here
}
-lean_lib «HashmapMain» {
+lean_lib «Base» {
-- add library configuration options here
}
-lean_lib «Base» {
+lean_lib «HashmapMain» {
-- add library configuration options here
}
-@[default_target]
-lean_exe «hashmap» {
- root := `Main
-}