diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/dumpglob.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index b8121af866..ca817b776b 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -25,23 +25,26 @@ let dump_string s = Pervasives.output_string !glob_file s type glob_output_t = - | None + | NoGlob | StdOut | MultFiles | File of string -let glob_output = ref MultFiles +let glob_output = ref NoGlob -let dump () = !glob_output != None +let dump () = !glob_output != NoGlob -let noglob () = glob_output := None +let noglob () = glob_output := NoGlob -let dump_to_stdout () = glob_output := StdOut +let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout let multi_dump () = !glob_output = MultFiles +let dump_to_dotglob f = glob_output := MultFiles + let dump_into_file f = glob_output := File f; open_glob_file f + let previous_state = ref MultFiles let pause () = previous_state := !glob_output let continue () = glob_output := !previous_state |