equal
deleted
inserted
replaced
63 [ "$#" -ne 0 ] && usage |
63 [ "$#" -ne 0 ] && usage |
64 |
64 |
65 |
65 |
66 ## main |
66 ## main |
67 |
67 |
68 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" browser || exit $?; } |
68 isabelle_admin_build browser || exit $? |
69 |
69 |
70 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" |
70 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" |
71 |
71 |
72 if [ -n "$GRAPHFILE" ]; then |
72 if [ -n "$GRAPHFILE" ]; then |
73 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |
73 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |