| changeset 74068 | 62e4ec8cff38 |
| parent 74061 | 203dfa8bc0fc |
| 74067:0b1462ce5fda | 74068:62e4ec8cff38 |
|---|---|
57 break; |
57 break; |
58 } |
58 } |
59 } |
59 } |
60 catch (Throwable exn) { |
60 catch (Throwable exn) { |
61 echo_err(Exn.print_error(exn)); |
61 echo_err(Exn.print_error(exn)); |
62 System.exit(Exn.return_code(exn, 2)); |
62 System.exit(Exn.failure_rc(exn)); |
63 } |
63 } |
64 } |
64 } |
65 } |
65 } |