author | wenzelm |
Mon, 12 May 1997 18:43:24 +0200 | |
changeset 3173 | 0013af1bc2c4 |
parent 3172 | 629d63c74ddc |
child 3174 | aceb79945d68 |
lib/Tools/doc | file | annotate | diff | comparison | revisions |
--- 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