changeset 2936 | bd33e7aae062 |
parent 2916 | d761a62da697 |
child 2940 | baae674b1d29 |
--- a/lib/Tools/doc Fri Apr 11 15:21:36 1997 +0200 +++ b/lib/Tools/doc Fri Apr 11 17:30:15 1997 +0200 @@ -30,7 +30,7 @@ ## args DOC="" -[ $# -ge 1 ] && { DOC="$1"; shift } +[ $# -ge 1 ] && { DOC="$1"; shift; } [ $# -ne 0 -o "$DOC" = "-?" ] && usage @@ -45,7 +45,7 @@ else for DIR in $ISABELLE_DOCS do - [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi } + [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; } done fail "Unknown Isabelle document: $DOC" fi