equal
deleted
inserted
replaced
15 PRG="$(basename "$0")" |
15 PRG="$(basename "$0")" |
16 |
16 |
17 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" |
17 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" |
18 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 |
18 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 |
19 |
19 |
20 ORIG_IFS="$IFS"; IFS=":"; declare -a TOOLS=($ISABELLE_TOOLS); IFS="$ORIG_IFS" |
20 splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}") |
21 |
21 |
22 |
22 |
23 ## diagnostics |
23 ## diagnostics |
24 |
24 |
25 function usage() |
25 function usage() |