diff options
| author | Hugo Herbelin | 2019-08-29 11:34:22 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-08-29 11:34:22 +0200 |
| commit | 8b1dc61c0885bb5a51bc4740255584c2a00d7511 (patch) | |
| tree | d7d793794ec97976d3339f21d722ee29d8e941df /interp/dumpglob.ml | |
| parent | 1ab00ddd8fa6ca5428c7f6ff56de0562bcb4ca1f (diff) | |
| parent | 61f4df8b5b974302e8b48bcf271aa68757db69fe (diff) | |
Merge PR #10643: [glob/aux files] Remove undocumented Stdout dump, cleanup flags.
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
Diffstat (limited to 'interp/dumpglob.ml')
| -rw-r--r-- | interp/dumpglob.ml | 32 |
1 files changed, 11 insertions, 21 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 8d6a266c30..41d1da9694 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -20,31 +20,21 @@ let open_glob_file f = let close_glob_file () = close_out !glob_file -type glob_output_t = - | NoGlob - | StdOut - | MultFiles - | Feedback - | File of string +type glob_output = + | NoGlob + | Feedback + | MultFiles + | File of string let glob_output = ref NoGlob -let dump () = !glob_output != NoGlob +let dump () = !glob_output <> NoGlob -let noglob () = glob_output := NoGlob - -let dump_to_dotglob () = glob_output := MultFiles - -let dump_into_file f = - if String.equal f "stdout" then - (glob_output := StdOut; glob_file := stdout) - else - (glob_output := File f; open_glob_file f) - -let feedback_glob () = glob_output := Feedback +let set_glob_output mode = + glob_output := mode let dump_string s = - if dump () && !glob_output != Feedback then + if dump () && !glob_output != Feedback then output_string !glob_file s let start_dump_glob ~vfile ~vofile = @@ -57,13 +47,13 @@ let start_dump_glob ~vfile ~vofile = | File f -> open_glob_file f; output_string !glob_file "DIGEST NO\n" - | NoGlob | Feedback | StdOut -> + | NoGlob | Feedback -> () let end_dump_glob () = match !glob_output with | MultFiles | File _ -> close_glob_file () - | NoGlob | Feedback | StdOut -> () + | NoGlob | Feedback -> () let previous_state = ref MultFiles let pause () = previous_state := !glob_output; glob_output := NoGlob |