Skip to content
Snippets Groups Projects
Commit 5c23e9ad authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Fix a bug causing frama-c and gcc paths with tilde not be expanded

parent e53fc335
No related branches found
No related tags found
No related merge requests found
...@@ -33,6 +33,14 @@ error () { ...@@ -33,6 +33,14 @@ error () {
fi fi
} }
# Check whether the first line reported by running command $1 has an identifier
# specified by $2. E.g., check whether readlink used by the script is GNU and
# getopt comes from util-linux.
required_tool() {
"$1" --version 2>&1 | head -1 | grep "$2" > /dev/null
error "$1 is not $2" $?
}
# Check if a given executable name can be found by in the PATH # Check if a given executable name can be found by in the PATH
has_tool() { has_tool() {
which "$@" >/dev/null 2>&1 && return 0 || return 1 which "$@" >/dev/null 2>&1 && return 0 || return 1
...@@ -281,13 +289,13 @@ do ...@@ -281,13 +289,13 @@ do
# Supply Frama-C executable name # Supply Frama-C executable name
-I|--frama-c) -I|--frama-c)
shift; shift;
OPTION_FRAMAC="$1" OPTION_FRAMAC="$(which $1)"
shift; shift;
;; ;;
# Supply GCC executable name # Supply GCC executable name
-G|--gcc) -G|--gcc)
shift; shift;
OPTION_CC="$1" OPTION_CC="$(which $1)"
shift; shift;
;; ;;
# Specify EACSL_SHARE directory (where C runtime library lives) by hand # Specify EACSL_SHARE directory (where C runtime library lives) by hand
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment