From 4db56fe2c963a4052f8415b3985c8765407fccbc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 17:49:03 +0100
Subject: Update the extraction of Lean files

---
 tests/lean/misc-loops/lakefile.lean | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

(limited to 'tests/lean/misc-loops/lakefile.lean')

diff --git a/tests/lean/misc-loops/lakefile.lean b/tests/lean/misc-loops/lakefile.lean
index 0d20ba1f..097c0a7d 100644
--- a/tests/lean/misc-loops/lakefile.lean
+++ b/tests/lean/misc-loops/lakefile.lean
@@ -4,15 +4,9 @@ open Lake DSL
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
-package «loops» {
-  -- add package configuration options here
-}
+package «loops» {}
 
-lean_lib «Base» {
-  -- add library configuration options here
-}
-
-lean_lib «Loops» {
-  -- add library configuration options here
-}
+lean_lib «Base» {}
 
+@[default_target]
+lean_lib «Loops» {}
-- 
cgit v1.2.3