diff options
Diffstat (limited to 'debugger/input_handling.ml')
| -rw-r--r-- | debugger/input_handling.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/debugger/input_handling.ml b/debugger/input_handling.ml index b043629bd1..e0dd6884ac 100644 --- a/debugger/input_handling.ml +++ b/debugger/input_handling.ml @@ -52,8 +52,7 @@ let execute_with_other_controller controller file funct = result with x -> - change_controller file old_controller; - raise x + cleanup x (change_controller file) old_controller (*** The "Main Loop" ***) @@ -84,8 +83,7 @@ let main_loop () = continue_main_loop := old_state with x -> - continue_main_loop := old_state; - raise x + cleanup x ((:=) continue_main_loop) old_state (*** Managing user inputs ***) |