# HG changeset patch
# User wenzelm
# Date 1354227170 -3600
# Node ID 735bea8d89c9d738659711b7eb0ba128047eb5c9
# Parent  5a1194acbecdfc1ca00e2ed82dca8348f1f4df4d
more defensive retry via fork;

diff -r 5a1194acbecd -r 735bea8d89c9 Admin/exec_process/exec_process.c
--- a/Admin/exec_process/exec_process.c	Thu Nov 29 18:05:41 2012 +0100
+++ b/Admin/exec_process/exec_process.c	Thu Nov 29 23:12:50 2012 +0100
@@ -39,8 +39,12 @@
 
   /* setsid */
 
-  if (getgid() == getpid()) fail("Cannot set session id");
-  setsid();
+  if (setsid() == -1) {
+    pid_t pid = fork();
+    if (pid == -1) fail("Cannot set session id (failed to fork)");
+    else if (pid != 0) exit(0);
+    else if (setsid() == -1) fail("Cannot set session id (after fork)");
+  }
 
 
   /* exec */