From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- interp/dumpglob.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/dumpglob.mli') diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index a7c79911..e84a6405 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -9,7 +9,7 @@ val open_glob_file : string -> unit val close_glob_file : unit -> unit -val start_dump_glob : string -> unit +val start_dump_glob : vfile:string -> vofile:string -> unit val end_dump_glob : unit -> unit val dump : unit -> bool -- cgit v1.2.3