r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

chore: disable LeanInk because of weird panics

main
Henrik 2023-06-25 15:14:43 +02:00
parent 76a137dabc
commit 9af4c720f0
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lakefile.lean
View File

@ -40,7 +40,7 @@ module_facet docs (mod) : FilePath := do
logInfo s!"Documenting module: {mod.name}" logInfo s!"Documenting module: {mod.name}"
proc { proc {
cmd := exeFile.toString cmd := exeFile.toString
args := #["single", mod.name.toString, "--ink"] args := #["single", mod.name.toString]
env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)] env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)]
} }
return (docFile, trace) return (docFile, trace)