equal
deleted
inserted
replaced
32 FAIL="" |
32 FAIL="" |
33 |
33 |
34 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" |
34 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" |
35 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
35 . "$ISABELLE_HOME/lib/scripts/timestart.bash" |
36 |
36 |
37 ORIG_IFS="$IFS"; IFS=":"; declare -a COMPONENTS=($ISABELLE_COMPONENTS); IFS="$ORIG_IFS" |
37 splitarray ":" "$ISABELLE_COMPONENTS"; COMPONENTS=("${SPLITARRAY[@]}") |
38 |
38 |
39 for DIR in "${COMPONENTS[@]}" |
39 for DIR in "${COMPONENTS[@]}" |
40 do |
40 do |
41 if [ -f "$DIR/IsaMakefile" ]; then |
41 if [ -f "$DIR/IsaMakefile" ]; then |
42 NAME="$(basename "$DIR")" |
42 NAME="$(basename "$DIR")" |