# HG changeset patch
# User wenzelm
# Date 863455404 -7200
# Node ID 0013af1bc2c45d424d1173dbca1a655880141781
# Parent  629d63c74ddc1abcf4d22d8dfc7170f8303d62c8
fixed ISABELLE_DOCS multiple components;

diff -r 629d63c74ddc -r 0013af1bc2c4 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