]> matita.cs.unibo.it Git - helm.git/commitdiff
kill HTTP child on exit
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 17 Jan 2003 16:07:09 +0000 (16:07 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 17 Jan 2003 16:07:09 +0000 (16:07 +0000)
helm/uwobo/src/ocaml/uwobo.ml

index 792e3e64ace55c57b448dff37256c87b4110682e..a0e9078a83f42d7676a61ab6fa1b098462467f3b 100644 (file)
@@ -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 ... *)