snapshot

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

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 83bdeb36f6ea3fcd55f6e7effc7635d00fad9ee2..1a55795a5536666d5c0adc993bdb5d1bcc1d7a13 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -45,3 +45,7 @@ let append_phrase_sep s =
   else
     s
 
+let strip_trailing_blanks =
+  let rex = Pcre.regexp "\\s*$" in
+  fun s -> Pcre.replace ~rex s
+