Tweak

vbeffara · Feb 28, 2024 · 30e7734 · 30e7734
1 parent 95f23fe
commit 30e7734
Showing 1 changed file with 3 additions and 5 deletions.
diff --git a/lakefile.lean b/lakefile.lean
@@ -3,21 +3,19 @@ open Lake DSL
 
 package «rMT4» {
   -- add any package configuration options here
-  moreLinkArgs := #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]
+  -- moreLinkArgs := #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]
 }
 
 require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
 
 -- require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.0.2"
 
-@[default_target]
-lean_lib RMT4 {
+@[default_target] lean_lib RMT4 {
   -- add any library configuration options here
   -- moreLinkArgs := #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]
 }
 
 require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"
 
-meta if get_config? env = some "dev" then
-require «doc-gen4» from git
+meta if get_config? env = some "dev" then require «doc-gen4» from git
   "https://github.com/leanprover/doc-gen4" @ "main"