aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib/util.ml4
-rw-r--r--lib/util.mli1
2 files changed, 3 insertions, 2 deletions
diff --git a/lib/util.ml b/lib/util.ml
index 117eeef1fe..3203d0f78b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -77,14 +77,14 @@ let rec raw_str_index i gdzie l c co cl =
if (i'+cl <= l) && (is_sub gdzie l i' co cl 0) then i' else
raw_str_index (i'+1) gdzie l c co cl
-let str_index_from gdzie i co =
+let string_index_from gdzie i co =
if co="" then i else
raw_str_index i gdzie (String.length gdzie)
(String.unsafe_get co 0) co (String.length co)
let string_string_contains ~where ~what =
try
- let _ = str_index_from where 0 what in true
+ let _ = string_index_from where 0 what in true
with
Not_found -> false
diff --git a/lib/util.mli b/lib/util.mli
index 23791fecb3..58d5150b72 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -57,6 +57,7 @@ val is_ident_tail : char -> bool
val explode : string -> string list
val implode : string list -> string
+val string_index_from : string -> int -> string -> int
val string_string_contains : where:string -> what:string -> bool
val parse_loadpath : string -> string list