--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Cygwin/exec_process.c Thu Apr 26 19:44:18 2012 +0200
@@ -0,0 +1,59 @@
+/* Author: Makarius
+
+Bash process group invocation on Cygwin.
+*/
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <sys/types.h>
+#include <unistd.h>
+#include <process.h>
+
+
+static void fail(const char *msg)
+{
+ printf("%s\n", msg);
+ exit(2);
+}
+
+
+int main(int argc, char *argv[])
+{
+ /* args */
+
+ if (argc != 3) {
+ printf("Bad arguments\n");
+ exit(1);
+ }
+ char *pid_name = argv[1];
+ char *script = argv[2];
+
+
+ /* report pid */
+
+ FILE *pid_file;
+ pid_file = fopen(pid_name, "w");
+ if (pid_file == NULL) fail("Cannot open pid file");
+ fprintf(pid_file, "%d", getpid());
+ fclose(pid_file);
+
+
+ /* setsid */
+
+ if (getgid() == getpid()) fail("Cannot set session id");
+ setsid();
+
+
+ /* exec */
+
+ char *cmd_line[4];
+ cmd_line[0] = "/bin/bash";
+ cmd_line[1] = "-c";
+ cmd_line[2] = script;
+ cmd_line[3] = NULL;
+
+ int pid = spawnv(_P_NOWAIT, "/bin/bash", cmd_line);
+ if (pid == -1) fail("Bad process");
+ waitpid(pid);
+}
+
--- a/src/Pure/Concurrent/bash.ML Thu Apr 26 14:42:50 2012 +0200
+++ b/src/Pure/Concurrent/bash.ML Thu Apr 26 19:44:18 2012 +0200
@@ -28,13 +28,19 @@
Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
let
val _ = File.write script_path script;
+ val bash_script =
+ "exec bash " ^
+ File.shell_path script_path ^
+ " > " ^ File.shell_path out_path ^
+ " 2> " ^ File.shell_path err_path;
val status =
OS.Process.system
- ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
- File.shell_path pid_path ^ " script \"exec bash " ^
- File.shell_path script_path ^
- " > " ^ File.shell_path out_path ^
- " 2> " ^ File.shell_path err_path ^ "\"");
+ (if getenv "EXEC_PROCESS" = "" then
+ ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^
+ File.shell_path pid_path ^ " script " ^ quote bash_script)
+ else
+ ("exec \"$EXEC_PROCESS\" " ^
+ File.shell_path pid_path ^ " " ^ quote bash_script));
val res =
(case Posix.Process.fromStatus status of
Posix.Process.W_EXITED => Result 0