diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
index 884dfb189ef701e5fe8a7ebe7d234fa76d4abe90..691002b883ef4ffa218c6e8b13f4a2c6bed81dfd 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -269,12 +269,10 @@ instrumentation- or compile-time error
 
 instrument foo.c and output the instrumented code to \fIa.out.frama.c\fP.
 
-.B e-acsl-gcc.sh -P -c -ogen_foo.c -Ofoo foo.c
+.B e-acsl-gcc.sh -c -ogen_foo.c -Ofoo foo.c
 
 instrument \fIfoo.c\fP, output the instrumented code to \fIgen_foo.c\fP and
 compile \fIfoo.c\fP into \fIfoo\fP and \fIgen_foo.c\fP into \fIfoo.e-acsl\fP.
-The \fB-P\fP option specifies that the instrumentation should omit debug
-functionality.
 
 .B e-acsl-gcc.sh --memory-model=bittree -C gen_foo.c
 
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
index 308b6c59819cea03c848907326a7443f808fa007..629ad4f4aec0751b8bf4bcd569d0428e77ec9d11 100644
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
@@ -29,7 +29,7 @@ _eacsl_gcc() {
   prev="${COMP_WORDS[COMP_CWORD-1]}"
 
   opts="
-    -i -C -d -o -O -v -V -f -E -L -M -l -e -g -q -s -F -P -N -D -I -G -X -a
+    -i -C -d -o -O -v -V -f -E -L -M -l -e -g -q -s -F -N -D -I -G -X -a
     -h -c -T -k
     --verbose= --debug= --debug-log= --logfile= --quiet --rt-debug --help
     --rt-verbose --check --then --keep-going --fail-with-code --external-assert=