From 2355ba85ee5201328e493c7de69747104ffcf203 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 10 Jun 2016 15:05:14 +0200
Subject: [PATCH] Comments in e-acsl-gcc.sh
---
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 7b7d7a5fdd2..ac409f88897 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"
--
GitLab