| piece::tl ->
let path = where ^ "/" ^ piece in
(try
- Unix.mkdir path 755
+ Unix.mkdir path 0o755
with
| Unix.Unix_error (Unix.EEXIST,_,_) -> ()
| Unix.Unix_error (e,_,_) -> raise (Failure (Unix.error_message e)));
let singleton f =
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
| [] -> []