diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index ae3dbbf7c2c909d161554c36f19295b23a70e2ff..ec919b1aa4338e53292f2dafaa55e3f0fe2df64d 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -1105,7 +1105,7 @@ if [ -n "$OPTION_COMPILE" ]; then # by a user if [ -n "$OPTION_INSTRUMENT" ]; then if [ -z "$OPTION_INSTRUMENTED_ONLY" ]; then - ($OPTION_ECHO; $CC $CPPFLAGS $CFLAGS "$@" -o "$OUTPUT_EXEC" $LDFLAGS); + ($OPTION_ECHO; $CC $CFLAGS $CPPFLAGS "$@" -o "$OUTPUT_EXEC" $LDFLAGS); error "fail to compile/link un-instrumented code" $?; fi # If $OPTION_INSTRUMENT is unset then the sources are assumed to be already