You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
53 lines
1.9 KiB
53 lines
1.9 KiB
From: Guillaume Brochu <guillaume.brochu@gmail.com> |
|
Date: Sat, 3 Nov 2018 07:42:06 -0400 |
|
Subject: gui-close_server |
|
|
|
gui: close_server now more robust to multiple gwd instances |
|
|
|
See Issue 547 upstream |
|
--- |
|
gui/gui.ml | 31 ++++++++++++++++++------------- |
|
1 file changed, 18 insertions(+), 13 deletions(-) |
|
|
|
diff --git a/gui/gui.ml b/gui/gui.ml |
|
index 254d4cb..f68b90d 100644 |
|
--- a/gui/gui.ml |
|
+++ b/gui/gui.ml |
|
@@ -284,19 +284,24 @@ value close_server conf = |
|
clean_waiting_pids conf; |
|
eprintf "Closing..."; flush stderr; |
|
(* Making a (empty) file STOP_SERVER to make the server stop. *) |
|
- let stop_server = |
|
- List.fold_left Filename.concat conf.bases_dir ["cnt"; "STOP_SERVER"] |
|
- in |
|
- let oc = open_out stop_server in |
|
- close_out oc; |
|
- (* Send a phony connection to unblock it. *) |
|
- let s = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in |
|
- try |
|
- Unix.connect s (Unix.ADDR_INET Unix.inet_addr_loopback conf.port) |
|
- with [ Unix.Unix_error _ _ _ -> () ]; |
|
- try Unix.close s with |
|
- [ Unix.Unix_error _ _ _ -> () ]; |
|
- ignore (Unix.waitpid [] server_pid); |
|
+ let (pid, ps) = Unix.waitpid [Unix.WNOHANG] server_pid in |
|
+ if pid=0 then |
|
+ let stop_server = |
|
+ List.fold_left Filename.concat conf.bases_dir ["cnt"; "STOP_SERVER"] |
|
+ in |
|
+ do { |
|
+ let oc = open_out stop_server in |
|
+ close_out oc; |
|
+ (* Send a phony connection to unblock it. *) |
|
+ let s = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in |
|
+ try |
|
+ Unix.connect s (Unix.ADDR_INET Unix.inet_addr_loopback conf.port) |
|
+ with [ Unix.Unix_error _ _ _ -> () ]; |
|
+ try Unix.close s with |
|
+ [ Unix.Unix_error _ _ _ -> () ]; |
|
+ ignore (Unix.waitpid [] server_pid); |
|
+ try Sys.remove stop_server with [ Sys_error _ -> () ] |
|
+ } else (); |
|
conf.server_running := None; |
|
eprintf "\n"; flush stderr; |
|
}
|
|
|