summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-07-03 18:52:46 +0100
committerAlasdair Armstrong2017-07-03 18:52:46 +0100
commit133823b7488174f0097685df6be0a0d172b23701 (patch)
tree26a712ccf0d295293109829f88087db7dcc7345c
parent8b8f868fc585ce94a9dbe6c39d9b14288f3a6611 (diff)
Fixed bug in XML output for jekins
-rwxr-xr-xtest/typecheck/run_tests.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index 8a5bc01b..a3829970 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -13,7 +13,7 @@ mkdir -p $DIR/rtpass
mkdir -p $DIR/lem
mkdir -p $DIR/rtfail
-rm $DIR/tests.xml
+rm -f $DIR/tests.xml
pass=0
fail=0