--- 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"