equal
deleted
inserted
replaced
23 [ "$#" -ne 0 ] && usage |
23 [ "$#" -ne 0 ] && usage |
24 |
24 |
25 declare -a LOGICS=() |
25 declare -a LOGICS=() |
26 declare -a ISABELLE_PATHS=() |
26 declare -a ISABELLE_PATHS=() |
27 |
27 |
28 ORIG_IFS="$IFS"; IFS=":"; ISABELLE_PATHS=($ISABELLE_PATH); IFS=$ORIG_IFS |
28 splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}") |
29 |
29 |
30 for DIR in "${ISABELLE_PATHS[@]}" |
30 for DIR in "${ISABELLE_PATHS[@]}" |
31 do |
31 do |
32 DIR="$DIR/$ML_IDENTIFIER" |
32 DIR="$DIR/$ML_IDENTIFIER" |
33 for FILE in "$DIR"/* |
33 for FILE in "$DIR"/* |