summaryrefslogtreecommitdiff
path: root/tests/lean/hashmap_on_disk/lakefile.lean
diff options
context:
space:
mode:
authorJonathan Protzenko2023-01-25 13:12:01 -0800
committerSon HO2023-06-04 21:44:33 +0200
commite1ee59f6a45482e93901f6a549f594fd6ef15234 (patch)
treec9d20fdc675823b058b7d364852c6a5d0bfaf729 /tests/lean/hashmap_on_disk/lakefile.lean
parentdee74ca1f90acb076289286f6f69df65e63604ce (diff)
New directory structure and corresponding extraction, + misc fixes, for Lean
Diffstat (limited to 'tests/lean/hashmap_on_disk/lakefile.lean')
-rw-r--r--tests/lean/hashmap_on_disk/lakefile.lean6
1 files changed, 5 insertions, 1 deletions
diff --git a/tests/lean/hashmap_on_disk/lakefile.lean b/tests/lean/hashmap_on_disk/lakefile.lean
index d2a31ffe..5b9adebb 100644
--- a/tests/lean/hashmap_on_disk/lakefile.lean
+++ b/tests/lean/hashmap_on_disk/lakefile.lean
@@ -5,7 +5,11 @@ package «hashmap» {
-- add package configuration options here
}
-lean_lib «Hashmap» {
+lean_lib «HashmapMain» {
+ -- add library configuration options here
+}
+
+lean_lib «Base» {
-- add library configuration options here
}