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/minilib.ml | |
| parent | 82f63ddf9c7d2fdd670f292f725a4295655db193 (diff) | |
Ide: Drop argument added by MacOS during .app launch
Diffstat (limited to 'ide/minilib.ml')
| -rw-r--r-- | ide/minilib.ml | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/ide/minilib.ml b/ide/minilib.ml index 6a960e266..d11e8c56b 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -6,6 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +let rec print_list print fmt = function + | [] -> () + | [x] -> print fmt x + | x :: r -> print fmt x; print_list print fmt r + type level = [ | `DEBUG | `INFO @@ -53,3 +58,13 @@ let coqide_config_dirs () = coqide_config_home () :: List.map coqify (Glib.get_system_config_dirs ()) @ Option.List.cons Coq_config.configdir [] + +let is_prefix_of pre s = + let i = ref 0 in + let () = while (!i < (String.length pre) + && !i < (String.length s) + && pre.[!i] = s.[!i]) do + incr i + done + in !i = String.length pre + |