michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(doc/lean/test_single): "race condition" when running tests in parallel

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-10 17:28:39 -07:00
parent d6d0593afb
commit d204d9c025
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/lean/test_single.sh
View file

@ -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