diff --git a/src/plugins/e-acsl/scripts/testrun.sh b/src/plugins/e-acsl/scripts/testrun.sh index 3d285b76d8f2aa80e0715ac47e43300eed6c6ab5..a24f4b5f27b7c62b2fd45aaf8b5fedb7a690d19a 100755 --- a/src/plugins/e-acsl/scripts/testrun.sh +++ b/src/plugins/e-acsl/scripts/testrun.sh @@ -90,7 +90,7 @@ error() { exit 1 } - # Do a clean-up on exit +# Do a clean-up on exit trap "clean" EXIT HUP INT QUIT TERM # Run executable and report results @@ -141,7 +141,7 @@ run_test() { # Run GMP tests if specified run_test "$EXTRA" -if test -n "$GMP"; then +if [ -n "$GMP" ]; then run_test "--gmp $EXTRA" fi exit 0