diff -r 998cb95fdd43 -r bd33e7aae062 lib/Tools/doc
--- 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