let obj_file_of_baseuri writable baseuri =
try
LibraryMisc.obj_file_of_baseuri
- ~must_exist:true ~baseuri ~writable
+ ~must_exist:true ~baseuri ~writable
with
| Http_getter_types.Unresolvable_URI _
| Http_getter_types.Key_not_found _ ->
LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
+ ~must_exist:false ~baseuri ~writable:true
;;
let main () =
let resolve alias current_buri =
let buri = buri alias in
if buri <> current_buri then Some buri else None in
- MatitaInit.fill_registry ();
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"];
- MatitaInit.parse_cmdline ();
- MatitaInit.load_configuration_file ();
+ MatitaInit.parse_cmdline_and_configuration_file ();
+ MatitaInit.initialize_environment ();
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