diff -r cb3c5189ea85 -r 468eff174a77 lib/Tools/doc
--- a/lib/Tools/doc	Fri Aug 21 19:06:12 2009 +0200
+++ b/lib/Tools/doc	Sat Aug 22 17:08:06 2009 +0200
@@ -34,7 +34,7 @@
 
 ## main
 
-ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS"
+splitarray ":" "$ISABELLE_DOCS"; DOCS=("${SPLITARRAY[@]}")
 
 if [ -z "$DOC" ]; then
   for DIR in "${DOCS[@]}"