~host:(Helm_registry.get "db.host")
~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database")
~host:(Helm_registry.get "db.host")
~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database")
- (fun suffix ->
- (*prerr_endline ("unregistering " ^ uri ^ suffix);*)
- Http_getter.unregister (uri ^ suffix))
-
+ (fun suffix ->
+ try
+ MatitaMisc.safe_remove (Http_getter.resolve (uri ^ suffix))
+ with Http_getter_types.Key_not_found _ -> ())
let name_tbl = MetadataTypes.name_tbl () in
let query = sprintf
"SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl
let name_tbl = MetadataTypes.name_tbl () in
let query = sprintf
"SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl