Skip to content

Commit

Permalink
fix?
Browse files Browse the repository at this point in the history
  • Loading branch information
RemyDegenne committed Feb 22, 2024
1 parent 790b9a7 commit ea7d8ab
Showing 1 changed file with 6 additions and 6 deletions.
12 changes: 6 additions & 6 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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"

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"

0 comments on commit ea7d8ab

Please sign in to comment.