diff --git a/lakefile.lean b/lakefile.lean index 2e17834..0c32e9d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -55,7 +55,7 @@ module_facet docs (mod) : FilePath := do logInfo s!"Documenting module: {mod.name}" proc { cmd := exeFile.toString - args := #["single", mod.name.toString, "--ink"] + args := #["single", mod.name.toString] env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)] } return (docFile, trace)