| #!/usr/bin/env bash | |
| awk 'BEGIN { lean = 0; idx = 0 } /```/ { if (lean == 1) lean = 0; } { if (lean == 1) { sub(/# /, ""); print $0 > out } } /```lean/ && !/```lean,ignore/ { lean = 1; idx = idx + 1; out = FILENAME "." idx ".lean" }' $1 | |
| for f in `ls $1.*.lean`; do | |
| echo "testing $f" | |
| cat $f | |
| if ! lean $f; then | |
| echo "FAILED" | |
| rm -f $1.*.lean | |
| exit 1 | |
| fi | |
| rm $f | |
| done |