let root,baseuri,_,_ =
Librarian.baseuri_of_script ~include_paths mafile
in
- let obj =
+ let obj_writeable, obj_read_only =
if Filename.check_suffix mafile ".mma" then
+ Filename.chop_suffix mafile ".mma" ^ ".ma",
Filename.chop_suffix mafile ".mma" ^ ".ma"
else
LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.obj_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:false
in
- Some root, obj
- with Librarian.NoRootFor x -> None, ""
+ Some root, obj_writeable, obj_read_only
+ with Librarian.NoRootFor x -> None, "", ""
;;
let mtime_of_source_object s =
;;
let build options fname =
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
let compile opts fname =
try
GrafiteSync.push ();
GrafiteParser.pop ();
GrafiteSync.pop ();
false
- | exn ->
+ | exn when not matita_debug ->
HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
assert false
in