chore: make CI fail if we panic (#246)

leanprover · Jan 4, 2025 · 535c69d · 535c69d
1 parent 9d993b2
commit 535c69d
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/test_docs.sh b/test_docs.sh
@@ -12,5 +12,7 @@ name = "«doc-gen4»"
 path = "../doc-gen4"
 EOL
 
+export LEAN_ABORT_ON_PANIC=1
+
 lake update doc-gen4
 lake build Batteries:docs