diff --git a/bin/frama-c-script b/bin/frama-c-script index 7fa99649748ed982c59e9c77344becc42367db9b..1aa49ad4b139b2cd1873eb5274338202f103e27d 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;