| changeset 34297 | 5c0a2583f997 |
| parent 34283 | 7911e83d06c0 |
| child 35587 | f037aa6699c3 |
--- a/lib/Tools/browser Sat Jan 09 16:31:19 2010 +0100 +++ b/lib/Tools/browser Sat Jan 09 18:22:40 2010 +0100 @@ -60,7 +60,7 @@ ## main -[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" browser +[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" browser || exit $?; } classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"