diff options
Diffstat (limited to 'debugger/question.ml')
| -rw-r--r-- | debugger/question.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/debugger/question.ml b/debugger/question.ml index 69e9ddbde1..0ecd63cb7a 100644 --- a/debugger/question.ml +++ b/debugger/question.ml @@ -44,8 +44,8 @@ let yes_or_no message = answer with x -> - current_prompt := old_prompt; - stop_user_input (); - raise x + cleanup x (fun () -> + current_prompt := old_prompt; + stop_user_input ()) () else false |