else
s
+let mkdir path =
+ let components = Str.split (Str.regexp "/") path in
+ let rec aux where = function
+ | [] -> ()
+ | piece::tl ->
+ let path = where ^ "/" ^ piece in
+ (try
+ Unix.mkdir path 0o755
+ with
+ | Unix.Unix_error (Unix.EEXIST,_,_) -> ()
+ | Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e)));
+ aux path tl
+ in
+ aux "" components
+
let strip_trailing_blanks =
let rex = Pcre.regexp "\\s*$" in
fun s -> Pcre.replace ~rex s
let instance = lazy (f ()) in
fun () -> Lazy.force instance
-let mkdir d =
- let errmsg = sprintf "Unable to create directory \"%s\"" d in
- try
- let dir = "mkdir -p " ^ d in
- (match Unix.system dir with
- | Unix.WEXITED 0 -> ()
- | Unix.WEXITED n ->
- MatitaLog.error ("'mkdir -p " ^ dir ^ "' failed with "^string_of_int n);
- failwith errmsg
- | Unix.WSIGNALED s
- | Unix.WSTOPPED s ->
- MatitaLog.error
- ("'mkdir -p " ^ dir ^ "' signaled with " ^ string_of_int s);
- failwith errmsg)
- with Unix.Unix_error _ as exc ->
- MatitaLog.error
- ("Unix error in makigin dir " ^ (MatitaExcPp.to_string exc));
- failwith errmsg
-
let get_proof_status status =
match status.proof_status with
| Incomplete_proof s -> s
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
| [] -> []