added split

[helm.git] / helm / matita / matitaMisc.mli

diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli
index 86c11249aaf26465949bf8eefaf15d2bbaf4eb68..dafd91387a8dee473897e6d0b71d127316635284 100644 (file)
--- a/helm/matita/matitaMisc.mli
+++ b/helm/matita/matitaMisc.mli
@@ -54,6 +54,9 @@ val append_phrase_sep: string -> string
 val strip_trailing_blanks: string -> string
 val strip_trailing_slash: string -> string
 
+  (* split a string at character, char defaults to ' ' *)
+val split: ?char:char -> string -> string list
+
 val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *)
 
   (** @raise Failure *)