summaryrefslogtreecommitdiff
path: root/libs
diff options
context:
space:
mode:
Diffstat (limited to 'libs')
-rw-r--r--libs/util.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/libs/util.ml b/libs/util.ml
index 88b916f..940fe3e 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -80,6 +80,14 @@ let uid =
fun () -> c := !c + 1; string_of_int !c
+(* String *)
+
+let is_suffix s sf =
+ let n = String.length s in
+ let k = String.length sf in
+ n >= k && sf = String.sub s (n-k) k
+
+
(* Time heavy functions *)
let times_k : (string, float) Hashtbl.t = Hashtbl.create 10