aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/minilib.mli
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-07-21 15:52:19 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-07-22 18:21:58 +0200
commit34b0bde46bd46ab4c467caccc7a6aebb5a999a74 (patch)
treeaca142bd1408d03ee6bf09aef8462e26e43cadb3 /ide/minilib.mli
parent82f63ddf9c7d2fdd670f292f725a4295655db193 (diff)
Ide: Drop argument added by MacOS during .app launch
Diffstat (limited to 'ide/minilib.mli')
-rw-r--r--ide/minilib.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/ide/minilib.mli b/ide/minilib.mli
index 0508dbf83..b7672c900 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -9,6 +9,8 @@
(** Some excerpts of Util and similar files to avoid depending on them
and hence on Compat and Camlp4 *)
+val print_list : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
+
type level = [
| `DEBUG
| `INFO
@@ -25,3 +27,4 @@ val log : ?level:level -> string -> unit
val coqide_config_home : unit -> string
val coqide_config_dirs : unit -> string list
val coqide_data_dirs : unit -> string list
+val is_prefix_of : string -> string -> bool