Skip to content

Commit 00c759d

Browse files
committed
chore: make CI fail if we panic
1 parent e837a30 commit 00c759d

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

test_docs.sh

+2
Original file line numberDiff line numberDiff line change
@@ -12,5 +12,7 @@ name = "«doc-gen4»"
1212
path = "../doc-gen4"
1313
EOL
1414

15+
export LEAN_ABORT_ON_PANIC=1
16+
1517
lake update doc-gen4
1618
lake build Batteries:docs

0 commit comments

Comments
 (0)