From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 17 Jan 2003 16:07:09 +0000 (+0000)
Subject: kill HTTP child on exit
X-Git-Tag: v0_3_99~14
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ec5094737abf5898aae30b1b71b5910c039c94bc;p=helm.git

kill HTTP child on exit
---

diff --git a/helm/uwobo/src/ocaml/uwobo.ml b/helm/uwobo/src/ocaml/uwobo.ml
index 792e3e64a..a0e9078a8 100644
--- a/helm/uwobo/src/ocaml/uwobo.ml
+++ b/helm/uwobo/src/ocaml/uwobo.ml
@@ -232,8 +232,12 @@ let main () =
   let styles = new Uwobo_styles.styles in
     (* (3) clean up actions *)
   let last_process = ref true in
+  let http_child = ref None in
   let die_nice () = (** at_exit callback *)
     if !last_process then begin
+      (match !http_child with
+      | None -> ()
+      | Some pid -> Unix.kill pid Sys.sigterm);
       syslogger#log `Notice (sprintf "%s is terminating, bye!" daemon_name);
       syslogger#disable;
       close_out logger_outchan
@@ -251,6 +255,7 @@ let main () =
     let (res_pipe_exit, res_pipe_entrance) = Unix.pipe () in
     match Unix.fork () with
     | child when child > 0 -> (* (4) parent: listen on cmd pipe for updates *)
+        http_child := Some child;
         let stop_http_daemon () =  (* kill child *)
           debug_print (sprintf "Grandparent: killing pid %d" child);
           Unix.kill child Sys.sigterm;  (* kill child ... *)