--- a/lib/Tools/browser Fri Aug 15 22:58:59 2008 +0200
+++ b/lib/Tools/browser Fri Aug 15 22:59:01 2008 +0200
@@ -61,11 +61,11 @@
## main
-export CLASSPATH="$(javapath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar")"
+classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
if [ -z "$GRAPHFILE" ]; then
[ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
- exec java GraphBrowser.GraphBrowser
+ javawrapper GraphBrowser.GraphBrowser
else
PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
if [ -n "$CLEAN" ]; then
@@ -83,9 +83,9 @@
esac
if [ -z "$OUTFILE" ]; then
- java GraphBrowser.GraphBrowser "$(javapath "$PRIVATE_FILE")"
+ javawrapper GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
else
- java GraphBrowser.Console "$(javapath "$PRIVATE_FILE")" "$(javapath "$OUTFILE")"
+ javawrapper GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
fi
RC="$?"