lib/Tools/browser
changeset 9788 df671fa2562a
parent 9237 161fb7f00414
child 9794 2be239143d42
     1.1 --- a/lib/Tools/browser	Fri Sep 01 17:48:31 2000 +0200
     1.2 +++ b/lib/Tools/browser	Fri Sep 01 17:50:36 2000 +0200
     1.3 @@ -1,11 +1,13 @@
     1.4  #!/bin/bash
     1.5  #
     1.6  # $Id$
     1.7 +# Author: Markus Wenzel, TU Muenchen
     1.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  #
    1.10  # DESCRIPTION: Isabelle graph browser
    1.11  
    1.12  
    1.13 -PRG=$(basename $0)
    1.14 +PRG=$(basename "$0")
    1.15  
    1.16  function usage()
    1.17  {
    1.18 @@ -42,14 +44,14 @@
    1.19  # args
    1.20  
    1.21  GRAPHFILE=""
    1.22 -[ $# -gt 0 ] && { GRAPHFILE="$1"; shift; }
    1.23 -[ $# -ne 0 ] && usage
    1.24 +[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; }
    1.25 +[ "$#" -ne 0 ] && usage
    1.26  
    1.27  
    1.28  ## main
    1.29  
    1.30 -export CLASSPATH=$ISABELLE_HOME/lib/browser
    1.31 -[ -z "$GRAPHFILE" ] && cd $ISABELLE_BROWSER_INFO
    1.32 +export CLASSPATH="$ISABELLE_HOME/lib/browser"
    1.33 +[ -z "$GRAPHFILE" ] && cd "$ISABELLE_BROWSER_INFO"
    1.34  
    1.35 -java GraphBrowser.GraphBrowser $GRAPHFILE
    1.36 +java GraphBrowser.GraphBrowser "$GRAPHFILE"
    1.37  [ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE"