diff --git a/test_docs.sh b/test_docs.sh index 9c8bbc5..449e6c0 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