From 00c759dc337d71c9079685e8dd6264f764670c0e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 12 Dec 2024 20:15:50 +0100
Subject: [PATCH] chore: make CI fail if we panic

---
 test_docs.sh | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test_docs.sh b/test_docs.sh
index 9c8bbc5a..449e6c05 100755
--- 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