diff --git a/lakefile.lean b/lakefile.lean index 7edfa3e..c0146b8 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -40,7 +40,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)