From 1cf7002d44ed02e171a2b52c3ae1d833291e2b0f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 29 Jul 2016 16:18:42 +0200
Subject: [PATCH] [scripts] always use EXTRA args for running e-acsl-gcc.sh in
runtest
---
src/plugins/e-acsl/scripts/testrun.sh | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/scripts/testrun.sh b/src/plugins/e-acsl/scripts/testrun.sh
index c5438175385..3158d01f559 100755
--- a/src/plugins/e-acsl/scripts/testrun.sh
+++ b/src/plugins/e-acsl/scripts/testrun.sh
@@ -52,7 +52,7 @@ GMP="$3" # Whether to issue an additional run with -e-acsl-gmp-only
EXTRA="$4" # Extra e-acsl-gcc.sh flags
DEBUG="$5" # Debug option
-EACSLGCC="$(dirname $0)/e-acsl-gcc.sh" # E-ACSL wrapper script
+EACSLGCC="$(dirname $0)/e-acsl-gcc.sh $EXTRA" # E-ACSL wrapper script
ROOTDIR="`readlink -f $(dirname $0)/../`" # Root directory of the repository
TESTDIR="$ROOTDIR/tests/$PREFIX" # Test suite directory
@@ -143,10 +143,10 @@ run_test() {
RUNS=$((RUNS+1))
}
-run_test "$EXTRA"
+run_test ""
# Run GMP tests if specified
if [ -n "$GMP" ]; then
- run_test "--gmp $EXTRA"
+ run_test "--gmp"
fi
exit 0
--
GitLab