diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-07-21 15:52:19 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-07-22 18:21:58 +0200 |
| commit | 34b0bde46bd46ab4c467caccc7a6aebb5a999a74 (patch) | |
| tree | aca142bd1408d03ee6bf09aef8462e26e43cadb3 /ide/ideutils.mli | |
| parent | 82f63ddf9c7d2fdd670f292f725a4295655db193 (diff) | |
Ide: Drop argument added by MacOS during .app launch
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 5877d1270..657e92869 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -40,9 +40,6 @@ val stock_to_widget : ?size:[`CUSTOM of int * int | Gtk.Tags.icon_size] -> GtkStock.id -> GObj.widget -open Format -val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit - val custom_coqtop : string option ref (* @return command to call coqtop - custom_coqtop if set |