]> matita.cs.unibo.it Git - helm.git/commitdiff
ensure connections get closed after having been served
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 29 May 2006 17:36:36 +0000 (17:36 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 29 May 2006 17:36:36 +0000 (17:36 +0000)
daemons/whelp/searchEngine.ml

index e98bfe3567bf3ae10ad9fc30a6e76417d5c2f948..bb8c722977f7b829e817ef6cc653e8266bc81b5c 100644 (file)
@@ -404,7 +404,7 @@ prerr_endline "VIVO";
          ^ " type")))
         req outchan
 
-let callback dbd (req: Http_types.request) outchan =
+let callback (dbd, (req: Http_types.request), outchan) =
   try
     debug_print (sprintf "Received request: %s" req#path);
     (match req#path with
@@ -482,6 +482,11 @@ let callback dbd (req: Http_types.request) outchan =
       let msg = MooglePp.pp_error "Uncaught exception" exn_string in
       send_results (`Error msg) req outchan
 
+let callback dbd req ch =
+  HExtlib.finally
+    (fun () -> try close_out ch with Sys_error _ -> ())
+    callback (dbd, req, ch)
+
 let restore_environment () =
   match
     Helm_registry.get_opt Helm_registry.string "search_engine.environment_dump"