diff options
Diffstat (limited to 'interp/dumpglob.mli')
| -rw-r--r-- | interp/dumpglob.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index edea94f0c..37370f6e1 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -15,8 +15,7 @@ val end_dump_glob : unit -> unit val dump : unit -> bool val noglob : unit -> unit -val dump_to_stdout : unit -> unit -val dump_into_file : string -> unit +val dump_into_file : string -> unit (** special handling of "stdout" *) val dump_to_dotglob : unit -> unit val pause : unit -> unit |