From 30e7734ed65c497dd6b261ed174241ed1d56f077 Mon Sep 17 00:00:00 2001 From: Vincent Beffara Date: Wed, 28 Feb 2024 15:15:05 +0100 Subject: [PATCH] Tweak --- lakefile.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 6790692..1734f0e 100644 --- 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"