diff options
Diffstat (limited to 'debugger')
| -rw-r--r-- | debugger/command_line.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debugger/command_line.ml b/debugger/command_line.ml index fa2c96b06c..7114b86949 100644 --- a/debugger/command_line.ml +++ b/debugger/command_line.ml @@ -205,7 +205,7 @@ let line_loop ppf line_buffer = !previous_line in previous_line := ""; - if interprete_line ppf line then + if interprete_line ppf line && !interactif then previous_line := line done with |