diff -r fb8c5a66dbe8 -r df671fa2562a lib/Tools/browser --- a/lib/Tools/browser Fri Sep 01 17:48:31 2000 +0200 +++ b/lib/Tools/browser Fri Sep 01 17:50:36 2000 +0200 @@ -1,11 +1,13 @@ #!/bin/bash # # $Id$ +# Author: Markus Wenzel, TU Muenchen +# License: GPL (GNU GENERAL PUBLIC LICENSE) # # DESCRIPTION: Isabelle graph browser -PRG=$(basename $0) +PRG=$(basename "$0") function usage() { @@ -42,14 +44,14 @@ # args GRAPHFILE="" -[ $# -gt 0 ] && { GRAPHFILE="$1"; shift; } -[ $# -ne 0 ] && usage +[ "$#" -gt 0 ] && { GRAPHFILE="$1"; shift; } +[ "$#" -ne 0 ] && usage ## main -export CLASSPATH=$ISABELLE_HOME/lib/browser -[ -z "$GRAPHFILE" ] && cd $ISABELLE_BROWSER_INFO +export CLASSPATH="$ISABELLE_HOME/lib/browser" +[ -z "$GRAPHFILE" ] && cd "$ISABELLE_BROWSER_INFO" -java GraphBrowser.GraphBrowser $GRAPHFILE +java GraphBrowser.GraphBrowser "$GRAPHFILE" [ -n "$GRAPHFILE" -a -n "$DELETE" ] && rm -f "$GRAPHFILE"