lib/Tools/browser
changeset 9788 df671fa2562a
parent 9237 161fb7f00414
child 9794 2be239143d42
--- 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"