| changeset 32390 | 468eff174a77 |
| parent 32322 | 45cb4a86eca2 |
| child 52427 | 9d1cc9a22177 |
--- 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[@]}"