changeset 74067 | 0b1462ce5fda |
parent 74031 | 09821ca262d3 |
child 74068 | 62e4ec8cff38 |
--- a/src/Tools/Setup/src/Exn.java Sun Jul 25 16:38:16 2021 +0200 +++ b/src/Tools/Setup/src/Exn.java Mon Jul 26 13:04:55 2021 +0200 @@ -27,11 +27,9 @@ return found_interrupt; } - public static int INTERRUPT_RETURN_CODE = 130; - public static int return_code(Throwable exn, int rc) { - return is_interrupt(exn) ? INTERRUPT_RETURN_CODE : rc; + return is_interrupt(exn) ? 130 : rc; }