From 1e16d444f544af2c8077cf6335a0caf6ff950844 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 27 Aug 2020 10:18:24 +0200
Subject: [PATCH] [e-acsl:script] remove useless line
---
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 1 -
1 file changed, 1 deletion(-)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 1ef4a37607d..c81e38218fb 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -557,7 +557,6 @@ do
--then)
shift;
OPTION_THEN=-then
- FRAMAC_FLAGS="$FRAMAC_FLAGS"
;;
# Extra E-ACSL options
--e-acsl-extra)
--
GitLab