# HG changeset patch # User kleing # Date 1081829470 -7200 # Node ID 8c846773878afcb06589a1ab371da72e516c35be # Parent 71b9ef3d047fc1967281cba1b958c9482e5eeec1 use .jar diff -r 71b9ef3d047f -r 8c846773878a lib/Tools/browser --- a/lib/Tools/browser Tue Apr 13 00:43:23 2004 +0200 +++ b/lib/Tools/browser Tue Apr 13 06:11:10 2004 +0200 @@ -62,7 +62,7 @@ ## main -export CLASSPATH="$ISABELLE_HOME/lib/browser" +export CLASSPATH="$ISABELLE_HOME/lib/browser/GraphBrowser.jar" if [ -z "$GRAPHFILE" ]; then cd "$ISABELLE_BROWSER_INFO" exec java GraphBrowser.GraphBrowser