From 62d0cf38b2eea1b6bd6e0beed79ba4ac004bab18 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Sun, 16 Jul 2023 14:45:38 -0600
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 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)