lib/Tools/browser
changeset 34297 5c0a2583f997
parent 34283 7911e83d06c0
child 35587 f037aa6699c3
equal deleted inserted replaced
34296:5f454603228b 34297:5c0a2583f997
    58 [ "$#" -ne 0 ] && usage
    58 [ "$#" -ne 0 ] && usage
    59 
    59 
    60 
    60 
    61 ## main
    61 ## main
    62 
    62 
    63 [ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" browser
    63 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" browser || exit $?; }
    64 
    64 
    65 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
    65 classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
    66 
    66 
    67 if [ -z "$GRAPHFILE" ]; then
    67 if [ -z "$GRAPHFILE" ]; then
    68   [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
    68   [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"