changeset 32390 | 468eff174a77 |
parent 32325 | 300b7d5d23d7 |
--- a/lib/Tools/makeall Fri Aug 21 19:06:12 2009 +0200 +++ b/lib/Tools/makeall Sat Aug 22 17:08:06 2009 +0200 @@ -34,7 +34,7 @@ echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" . "$ISABELLE_HOME/lib/scripts/timestart.bash" -ORIG_IFS="$IFS"; IFS=":"; declare -a COMPONENTS=($ISABELLE_COMPONENTS); IFS="$ORIG_IFS" +splitarray ":" "$ISABELLE_COMPONENTS"; COMPONENTS=("${SPLITARRAY[@]}") for DIR in "${COMPONENTS[@]}" do