From f0949d579256d98a6695e1e566fc729e8deb4987 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 9 Jun 2020 10:42:26 +0200
Subject: [PATCH] [Analysis-scripts] update make-path
---
bin/frama-c-script | 11 +++++++----
1 file changed, 7 insertions(+), 4 deletions(-)
diff --git a/bin/frama-c-script b/bin/frama-c-script
index 7fa99649748..1aa49ad4b13 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -121,17 +121,20 @@ open_file() {
}
make_path() {
- cat <<EOF > frama-c-path.mk
+ dir=".frama-c"
+ if [ "$#" -gt 0 ]; then
+ dir="$1"
+ fi
+ cat <<EOF > "${dir}/path.mk"
FRAMAC_DIR=${DIR}
ifeq (\$(wildcard \$(FRAMAC_DIR)),)
# Frama-C not installed locally; using the version in the PATH
else
FRAMAC=\$(FRAMAC_DIR)/frama-c
FRAMAC_GUI=\$(FRAMAC_DIR)/frama-c-gui
-FRAMAC_CONFIG=\$(FRAMAC_DIR)/frama-c-config
endif
EOF
- echo "Wrote to: frama-c-path.mk"
+ echo "Wrote to: ${dir}/path.mk"
}
flamegraph() {
@@ -237,7 +240,7 @@ case "$command" in
;;
"make-path")
shift;
- make_path;
+ make_path "$@";
;;
"list-files")
shift;
--
GitLab