lib/Tools/doc

--- a/lib/Tools/doc	Mon May 12 18:34:49 1997 +0200
+++ b/lib/Tools/doc	Mon May 12 18:43:24 1997 +0200
@@ -34,13 +34,15 @@
 
 ## main
 
+DOCS=$(echo $ISABELLE_DOCS | tr : " ")
+
 if [ -z "$DOC" ]; then
-  for DIR in $ISABELLE_DOCS
+  for DIR in $DOCS
   do
     [ -f $DIR/Contents ] && cat $DIR/Contents
   done
 else
-  for DIR in $ISABELLE_DOCS
+  for DIR in $DOCS
   do
     [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
   done