diff options
Diffstat (limited to 'ide/coqide.mli')
| -rw-r--r-- | ide/coqide.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.mli b/ide/coqide.mli index cac6878cd..dd3995eb9 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -10,7 +10,7 @@ command line, initialize the load path, load the input state, load the files given on the command line, load the ressource file, produce the output state if any, and finally will launch the interface. *) -val sup_args : string ref +val sup_args : string list ref val do_load : string -> unit val process_argv : string list -> string list val crash_save : int -> unit |