Add doc-gen4

ImperialCollegeLondon · Nov 25, 2023 · 48860d8 · 48860d8
1 parent da34ffc
commit 48860d8
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/lakefile.lean b/lakefile.lean
@@ -8,6 +8,11 @@ package «FLT» {
 require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"
 
+-- This is run only if we're in `dev` mode. This is so not everyone has to build doc-gen
+meta if get_config? env = some "dev" then
+require «doc-gen4» from git
+ "https://github.com/leanprover/doc-gen4" @ "main"
+
 @[default_target]
 lean_lib «FLT» {
  -- add any library configuration options here