From 0d8433a5e7a2d1e91512a6422506dbd19241d128 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 12:31:18 +0100
Subject: Automate the generation of the lakefile.lean files

---
 tests/lean/hashmap_on_disk/lakefile.lean | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'tests/lean')

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
-}
-- 
cgit v1.2.3