changeset 62937 | d5e7a76ec1a6 |
parent 62923 | 3a122e1e352a |
child 78705 | fde0b195cb7d |
--- a/src/Pure/ML/exn_debugger.ML Sat Apr 09 20:18:15 2016 +0200 +++ b/src/Pure/ML/exn_debugger.ML Sat Apr 09 20:31:46 2016 +0200 @@ -31,7 +31,7 @@ val _ = Thread_Data.put trace_var NONE; in trace end; -val _ = ML_Debugger.on_exit_exception (SOME update_trace); +val _ = PolyML.DebuggerInterface.setOnExitException (SOME update_trace); (* capture exception trace *)