lib/Tools/doc
changeset 2936 bd33e7aae062
parent 2916 d761a62da697
child 2940 baae674b1d29
     1.1 --- a/lib/Tools/doc	Fri Apr 11 15:21:36 1997 +0200
     1.2 +++ b/lib/Tools/doc	Fri Apr 11 17:30:15 1997 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  ## args
     1.5  
     1.6  DOC=""
     1.7 -[ $# -ge 1 ] && { DOC="$1"; shift }
     1.8 +[ $# -ge 1 ] && { DOC="$1"; shift; }
     1.9  
    1.10  [ $# -ne 0 -o "$DOC" = "-?" ] && usage
    1.11  
    1.12 @@ -45,7 +45,7 @@
    1.13  else
    1.14    for DIR in $ISABELLE_DOCS
    1.15    do
    1.16 -    [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi }
    1.17 +    [ -f $DIR/$DOC.dvi ] && { cd $DIR; exec $DVI_VIEWER $DOC.dvi; }
    1.18    done
    1.19    fail "Unknown Isabelle document: $DOC"  
    1.20  fi