equal
deleted
inserted
replaced
32 [ "$#" -ne 0 -o "$DOC" = "-?" ] && usage |
32 [ "$#" -ne 0 -o "$DOC" = "-?" ] && usage |
33 |
33 |
34 |
34 |
35 ## main |
35 ## main |
36 |
36 |
37 ORIG_IFS="$IFS"; IFS=":"; declare -a DOCS=($ISABELLE_DOCS); IFS="$ORIG_IFS" |
37 splitarray ":" "$ISABELLE_DOCS"; DOCS=("${SPLITARRAY[@]}") |
38 |
38 |
39 if [ -z "$DOC" ]; then |
39 if [ -z "$DOC" ]; then |
40 for DIR in "${DOCS[@]}" |
40 for DIR in "${DOCS[@]}" |
41 do |
41 do |
42 [ -d "$DIR" ] || fail "Bad document directory: $DIR" |
42 [ -d "$DIR" ] || fail "Bad document directory: $DIR" |