From d204d9c025bcba4ad67f7678cacd2818b1fc43a4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 10 Oct 2014 17:28:39 -0700
Subject: [PATCH] fix(doc/lean/test_single): "race condition" when running
 tests in parallel

---
 doc/lean/test_single.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/lean/test_single.sh b/doc/lean/test_single.sh
index 1de2a952b..58724ff92 100755
--- a/doc/lean/test_single.sh
+++ b/doc/lean/test_single.sh
@@ -35,6 +35,6 @@ while read -r line; do
         echo -E "$line" >> $f.$i.lean
     fi
 done < $f
-rm -f *.produced.out
-rm -f *.lean
+rm -f $f.*.produced.out
+rm -f $f.*.lean
 exit 0