diff --git a/doc/test b/doc/test
index 5fd238cf9a..cf58589355 100755
--- a/doc/test
+++ b/doc/test
@@ -1,2 +1,11 @@
 #!/usr/bin/env bash
-awk 'BEGIN { lean = 0 } /```/ { if (lean == 1) lean = 0; } { if (lean == 1) { sub(/# /, ""); print $0 } } /```lean/ && !/```lean,ignore/ { lean = 1 }' $1 | lean --stdin
+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"
+  if ! lean $f; then
+      echo "FAILED"
+      rm -f $1.*.lean
+      exit 1
+  fi
+  rm $f
+done