diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index 7b7d7a5fdd23ba18e8a360c1812c57abdbbff095..ac409f8889760d0aaf9c4abb1ac7ad2c82e2c7c4 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -216,6 +216,7 @@ do OPTION_OUTPUT_EXEC="$1" shift ;; + # Specify the output name of the E-ACSL generated executable --oexec-e-acsl) shift; OPTION_EACSL_OUTPUT_EXEC="$1"