equal
deleted
inserted
replaced
64 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" |
64 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" |
65 |
65 |
66 if [ -z "$GRAPHFILE" ]; then |
66 if [ -z "$GRAPHFILE" ]; then |
67 [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" |
67 [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO" |
68 javawrapper GraphBrowser.GraphBrowser |
68 javawrapper GraphBrowser.GraphBrowser |
|
69 RC="$?" |
69 else |
70 else |
70 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |
71 PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE") |
71 if [ -n "$CLEAN" ]; then |
72 if [ -n "$CLEAN" ]; then |
72 mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
73 mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
73 else |
74 else |