| changeset 62505 | 9e2a65912111 |
| parent 62504 | f14f17e656a6 |
| child 62516 | 5732f1c31566 |
--- a/src/Pure/Tools/debugger.ML Thu Mar 03 14:03:06 2016 +0100 +++ b/src/Pure/Tools/debugger.ML Thu Mar 03 15:23:02 2016 +0100 @@ -33,7 +33,7 @@ fun error_wrapper e = e () handle exn => - if Exn.is_interrupt exn then reraise exn + if Exn.is_interrupt exn then Exn.reraise exn else error_message (Runtime.exn_message exn);