]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter_map.ml
- added maps sync
[helm.git] / helm / http_getter / http_getter_map.ml
index 07c2c10b4a0db1c667bfa4eef2edabb985cd3ce3..7a5ed1a3bc93ca1490b607f7574bd65e78acffde 100644 (file)
@@ -66,6 +66,12 @@ class map dbname =
         Dbm.iter f db
       ))
 
+    method sync =
+      self#doWriter (lazy (
+        Dbm.close db;
+        db <- open_dbm ()
+      ))
+
     method clear =
       self#doWriter (lazy (
         Dbm.close db;