From e29cc367f3c1e8e36ae4249f27bfe9e1c4ac6cc0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Nov 2020 13:51:52 -0800
Subject: [PATCH] feat: test each example using a separate file

---
 doc/test | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

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