From d26a2b0c610370cbae000a1ca0002b391c6095a1 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 8 Feb 2021 18:25:06 +0100
Subject: [PATCH] [eacsl] Remove mention of -P option in wrapper script
The `-P` option does not exist.
---
src/plugins/e-acsl/man/e-acsl-gcc.sh.1 | 4 +---
src/plugins/e-acsl/scripts/e-acsl-gcc.comp | 2 +-
2 files changed, 2 insertions(+), 4 deletions(-)
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 884dfb189ef..691002b883e 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 308b6c59819..629ad4f4aec 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=
--
GitLab