equal
deleted
inserted
replaced
57 |
57 |
58 |
58 |
59 function build_browser () |
59 function build_browser () |
60 { |
60 { |
61 pushd "$ISABELLE_HOME/lib/browser" >/dev/null |
61 pushd "$ISABELLE_HOME/lib/browser" >/dev/null |
62 "$ISABELLE_TOOL" env ./build || fail "Failed!" |
62 "$ISABELLE_TOOL" env ./build || exit $? |
63 popd >/dev/null |
63 popd >/dev/null |
64 } |
64 } |
65 |
65 |
66 |
66 |
67 function build_doc () |
67 function build_doc () |
82 |
82 |
83 |
83 |
84 function build_jars () |
84 function build_jars () |
85 { |
85 { |
86 pushd "$ISABELLE_HOME/src/Pure" >/dev/null |
86 pushd "$ISABELLE_HOME/src/Pure" >/dev/null |
87 "$ISABELLE_TOOL" env ./build-jars || fail "Failed!" |
87 "$ISABELLE_TOOL" env ./build-jars || exit $? |
88 popd >/dev/null |
88 popd >/dev/null |
89 } |
89 } |
90 |
90 |
91 |
91 |
92 ## main |
92 ## main |