]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/searchEngine.ml
ported to latest registry interface
[helm.git] / helm / searchEngine / searchEngine.ml
index afb274f460e07f008d746d2fee0be5ac3f8182c0..dcaee2466dc13a0c4a61c22d0de3ff1c5ee45d27 100644 (file)
@@ -467,7 +467,7 @@ let callback dbd (req: Http_types.request) outchan =
 
 let restore_environment () =
   match
-    Helm_registry.get_opt Helm_registry.get "search_engine.environment_dump"
+    Helm_registry.get_opt Helm_registry.string "search_engine.environment_dump"
   with
   | None -> ()
   | Some fname ->