method dump = db
method set_dump v = {< db = v >}
method set_dumpable_status
- : 'status. #g_dumpable_status as 'status -> 'self
+ : 'status. (#g_dumpable_status as 'status) -> 'self
= fun o -> {< db = o#dump >}
end
let ch = open_out (ng_path_of_baseuri baseuri) in
Marshal.to_channel ch (magic,(status#dump.dependencies,status#dump.objs)) [];
close_out ch;
-(*
+
+ if Helm_registry.get_bool "matita.remove_old_objects" then
remove_objects ~baseuri; (* FG: we remove the old objects before putting the new ones*)
-*)
+
List.iter
(function
| `Obj (uri,obj) ->