with
| Http_getter_types.Unresolvable_URI _
| Http_getter_types.Key_not_found _ ->
LibraryMisc.obj_file_of_baseuri
with
| Http_getter_types.Unresolvable_URI _
| Http_getter_types.Key_not_found _ ->
LibraryMisc.obj_file_of_baseuri
let dot_file = ref "" in
MatitaInit.add_cmdline_spec
["-dot", Arg.Set_string dot_file,
"<file> Save dependency graph in dot format to the given file"];
let dot_file = ref "" in
MatitaInit.add_cmdline_spec
["-dot", Arg.Set_string dot_file,
"<file> Save dependency graph in dot format to the given file"];
let include_paths =
Helm_registry.get_list Helm_registry.string "matita.includes" in
let args = Helm_registry.get_list Helm_registry.string "matita.args" in
let include_paths =
Helm_registry.get_list Helm_registry.string "matita.includes" in
let args = Helm_registry.get_list Helm_registry.string "matita.args" in
if not (Http_getter_storage.is_legacy baseuri) then
(let moo_file = obj_file_of_baseuri false baseuri in
Hashtbl.add include_deps ma_file moo_file;
if not (Http_getter_storage.is_legacy baseuri) then
(let moo_file = obj_file_of_baseuri false baseuri in
Hashtbl.add include_deps ma_file moo_file;