lib/Tools/doc
changeset 32390 468eff174a77
parent 32322 45cb4a86eca2
child 52427 9d1cc9a22177
     1.1 --- a/lib/Tools/doc	Fri Aug 21 19:06:12 2009 +0200
     1.2 +++ b/lib/Tools/doc	Sat Aug 22 17:08:06 2009 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 -ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS"
     1.8 +splitarray ":" "$ISABELLE_DOCS"; DOCS=("${SPLITARRAY[@]}")
     1.9  
    1.10  if [ -z "$DOC" ]; then
    1.11    for DIR in "${DOCS[@]}"