lib/Tools/doc
changeset 3173 0013af1bc2c4
parent 3007 e5efa177ee0c
child 8130 b077b79061b6
     1.1 --- a/lib/Tools/doc	Mon May 12 18:34:49 1997 +0200
     1.2 +++ b/lib/Tools/doc	Mon May 12 18:43:24 1997 +0200
     1.3 @@ -34,13 +34,15 @@
     1.4  
     1.5  ## main
     1.6  
     1.7 +DOCS=$(echo $ISABELLE_DOCS | tr : " ")
     1.8 +
     1.9  if [ -z "$DOC" ]; then
    1.10 -  for DIR in $ISABELLE_DOCS
    1.11 +  for DIR in $DOCS
    1.12    do
    1.13      [ -f $DIR/Contents ] && cat $DIR/Contents
    1.14    done
    1.15  else
    1.16 -  for DIR in $ISABELLE_DOCS
    1.17 +  for DIR in $DOCS
    1.18    do
    1.19      [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
    1.20    done