From 535c69d52d2359e7973c9c7bdc4041845dfab27e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 4 Jan 2025 13:50:31 +0100 Subject: [PATCH] chore: make CI fail if we panic (#246) --- 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