diff options
| author | Gabriel Scherer <gabriel.scherer@gmail.com> | 2023-03-23 22:59:26 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-03-23 22:59:26 +0100 |
| commit | 33d1461c340a6083da3e3aea62f99c16561367c1 (patch) | |
| tree | 4e3cb4c43a1c531a33920d1047ab56f62775e400 /debugger | |
| parent | dab4e3dc969c902f7d84f8690df8ac975f46a75a (diff) | |
| parent | c730d95d2c43e43664e1aaec58fdd439e212e363 (diff) | |
| download | ocaml-33d1461c340a6083da3e3aea62f99c16561367c1.tar.gz | |
Merge pull request #12088 from damiendoligez/fix-11949
one-line fix for #9265, #11949
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 |