]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter.ml
clean_cache method added
[helm.git] / helm / http_getter / http_getter.ml
index 0792d30b52a8a58ada989efe6570d3f01ab30dcd..48c82f8eaae356ba2f7f5218c35600b4dc1720b0 100644 (file)
@@ -387,6 +387,9 @@ let callback (req: Http_types.request) outchan =
             register uri url;
             return_html_msg "Register done" outchan
         | _ -> assert false)
+    | "/clean_cache" ->
+        Http_getter_cache.clean ();
+        return_html_msg "Done." outchan
     | "/update" ->
         Http_getter_env.reload (); (* reload servers list from servers file *)
         let log = update_from_all_servers () in