diff options
Diffstat (limited to 'interp/dumpglob.ml')
| -rw-r--r-- | interp/dumpglob.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 74c60f75b..1a44fac6c 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -30,11 +30,13 @@ let dump () = !glob_output != NoGlob let noglob () = glob_output := NoGlob -let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout - let dump_to_dotglob () = glob_output := MultFiles -let dump_into_file f = glob_output := File f; open_glob_file f +let dump_into_file f = + if String.equal f "stdout" then + (glob_output := StdOut; glob_file := Pervasives.stdout) + else + (glob_output := File f; open_glob_file f) let dump_string s = if dump () then Pervasives.output_string !glob_file s |