From ea7d8ab115adb0f6b632eff624b60462b4c60179 Mon Sep 17 00:00:00 2001 From: RemyDegenne Date: Thu, 22 Feb 2024 20:01:02 +0100 Subject: [PATCH] fix? --- lakefile.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/lakefile.lean b/lakefile.lean index 540d2a51..80479ebf 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,9 +15,9 @@ require mathlib from git @[default_target] lean_lib «TestingLowerBounds» where -- add any library configuration options here - -require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" - -meta if get_config? env = some "dev" then -require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "main" \ No newline at end of file + +require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" + +meta if get_config? env = some "dev" then +require «doc-gen4» from git + "https://github.com/leanprover/doc-gen4" @ "main"