From a888f480029a073f9b5a71a9a9dc10904efb7657 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 7 Apr 2003 13:24:16 +0000 Subject: [PATCH] added "replace" method which interfaces Dbm.replace function --- helm/http_getter/http_getter_map.ml | 5 +++++ helm/http_getter/http_getter_map.mli | 1 + 2 files changed, 6 insertions(+) diff --git a/helm/http_getter/http_getter_map.ml b/helm/http_getter/http_getter_map.ml index 06699f178..b7ac1c605 100644 --- a/helm/http_getter/http_getter_map.ml +++ b/helm/http_getter/http_getter_map.ml @@ -48,6 +48,11 @@ class map dbname = with Dbm.Dbm_error "Entry already exists" -> raise (Key_already_in key) )) + method replace key value = + self#doWriter (lazy ( + Dbm.replace db key value + )) + method remove key = self#doWriter (lazy ( try diff --git a/helm/http_getter/http_getter_map.mli b/helm/http_getter/http_getter_map.mli index ae9cf319f..720484f31 100644 --- a/helm/http_getter/http_getter_map.mli +++ b/helm/http_getter/http_getter_map.mli @@ -33,6 +33,7 @@ class map: string -> object method add: string -> string -> unit + method replace: string -> string -> unit method remove: string -> unit method resolve: string -> string method iter: (string -> string -> unit) -> unit -- 2.39.2