From 9af4c720f08e9c694e574fc35cf59b385be47175 Mon Sep 17 00:00:00 2001
From: Henrik <hargonix@gmail.com>
Date: Sun, 25 Jun 2023 15:14:43 +0200
Subject: [PATCH] chore: disable LeanInk because of weird panics

---
 lakefile.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)