diff -r cb3c5189ea85 -r 468eff174a77 lib/Tools/makeall
--- 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