remove matitamake binaries on clean

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

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index ca8dc2446660ec11d5e424119f53be2ff4ebd6a4..78e780a155224da1ee8b24a0c042cf34a9595dbe 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -26,9 +26,11 @@
 open Printf
 open MatitaTypes 
 
-let strip_trailing_slash =
-  let rex = Pcre.regexp "/$" in
-  fun s -> Pcre.replace ~rex s
+(** Functions "imported" from Http_getter_misc *)
+
+let strip_trailing_slash = Http_getter_misc.strip_trailing_slash
+let normalize_dir = Http_getter_misc.normalize_dir
+let strip_suffix = Http_getter_misc.strip_suffix
 
 let baseuri_of_baseuri_decl st =
   match st with
@@ -129,9 +131,9 @@ let mkdir path =
   in
   aux "" components
 
-let strip_trailing_blanks =
-  let rex = Pcre.regexp "\\s*$" in
-  fun s -> Pcre.replace ~rex s
+let trim_blanks =
+  let rex = Pcre.regexp "^\\s*(.*?)\\s*$" in
+  fun s -> (Pcre.extract ~rex s).(1)
 
 let split ?(char = ' ') s =
   let pieces = ref [] in
@@ -291,8 +293,9 @@ let obj_file_of_baseuri baseuri =
   path ^ ".moo"
 
 let obj_file_of_script f =
- let baseuri = baseuri_of_file f in
-  obj_file_of_baseuri baseuri
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+  let baseuri = baseuri_of_file f in
+   obj_file_of_baseuri baseuri
 
 let rec list_uniq = function 
   | [] -> []