| changeset 74067 | 0b1462ce5fda |
| parent 74031 | 09821ca262d3 |
| child 74068 | 62e4ec8cff38 |
| 74066:b3f072aa4690 | 74067:0b1462ce5fda |
|---|---|
25 e = e.getCause(); |
25 e = e.getCause(); |
26 } |
26 } |
27 return found_interrupt; |
27 return found_interrupt; |
28 } |
28 } |
29 |
29 |
30 public static int INTERRUPT_RETURN_CODE = 130; |
|
31 |
|
32 public static int return_code(Throwable exn, int rc) |
30 public static int return_code(Throwable exn, int rc) |
33 { |
31 { |
34 return is_interrupt(exn) ? INTERRUPT_RETURN_CODE : rc; |
32 return is_interrupt(exn) ? 130 : rc; |
35 } |
33 } |
36 |
34 |
37 |
35 |
38 /* message */ |
36 /* message */ |
39 |
37 |