changeset 34283 | 7911e83d06c0 |
parent 34282 | 549969a7f582 |
child 34284 | 33ad3571ad83 |
--- a/Admin/build Wed Jan 06 20:00:22 2010 +0100 +++ b/Admin/build Wed Jan 06 22:18:52 2010 +0100 @@ -58,12 +58,9 @@ function build_browser () { - echo "###" - echo "### Building graph browser ..." - echo "###" - - cd "$ISABELLE_HOME/lib/browser" - make clean all || fail "Failed to build graph browser!" + pushd "$ISABELLE_HOME/lib/browser" >/dev/null + "$ISABELLE_TOOL" env ./build || fail "Failed!" + popd >/dev/null }