universal component exec_process -- avoids special Admin/components/windows and might actually improve stability of forked processes (without using perl);
--- a/Admin/Windows/exec_process/build Wed Sep 19 17:27:37 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-#!/usr/bin/env bash
-#
-# Multi-platform build script
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-PRG="$(basename "$0")"
-
-
-# diagnostics
-
-function usage()
-{
- echo
- echo "Usage: $PRG TARGET"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-# command line args
-
-[ "$#" -eq 0 ] && usage
-TARGET="$1"; shift
-
-[ "$#" -eq 0 ] || usage
-
-
-# main
-
-mkdir -p "$TARGET"
-
-case "$TARGET" in
- x86_64-linux | x86_64-darwin)
- cc -m64 exec_process.c -o "$TARGET/exec_process"
- ;;
- x86-linux | x86-darwin)
- cc -m32 exec_process.c -o "$TARGET/exec_process"
- ;;
- x86-cygwin)
- cc exec_process.c -o "$TARGET/exec_process.exe"
- ;;
- *)
- cc exec_process.c -o "$TARGET/exec_process"
- ;;
-esac
-
-
--- a/Admin/Windows/exec_process/etc/settings Wed Sep 19 17:27:37 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-EXEC_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}/exec_process"
--- a/Admin/Windows/exec_process/exec_process.c Wed Sep 19 17:27:37 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-/* Author: Makarius
-
-Bash process group invocation.
-*/
-
-#include <stdlib.h>
-#include <stdio.h>
-#include <sys/types.h>
-#include <unistd.h>
-
-
-static void fail(const char *msg)
-{
- fprintf(stderr, "%s\n", msg);
- exit(2);
-}
-
-
-int main(int argc, char *argv[])
-{
- /* args */
-
- if (argc != 3) {
- fprintf(stderr, "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;
-
- execv("/bin/bash", cmd_line);
- fail("Cannot exec process");
-}
-
--- a/Admin/component_repository/components.sha1 Wed Sep 19 17:27:37 2012 +0200
+++ b/Admin/component_repository/components.sha1 Wed Sep 19 18:01:48 2012 +0200
@@ -1,5 +1,6 @@
2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
+6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz
ae7ee5becb26512f18c609e83b34612918bae5f0 exec_process-1.0.tar.gz
683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
--- a/Admin/components/main Wed Sep 19 17:27:37 2012 +0200
+++ b/Admin/components/main Wed Sep 19 18:01:48 2012 +0200
@@ -1,6 +1,7 @@
#main components for everyday use, without big impact on overall build time
cvc3-2.4.1
e-1.5
+exec_process-1.0.1
jdk-7u6
jedit_build-20120903
kodkodi-1.2.16
--- a/Admin/components/windows Wed Sep 19 17:27:37 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-#specific components for Windows/Cygwin only
-exec_process-1.0
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/exec_process/build Wed Sep 19 18:01:48 2012 +0200
@@ -0,0 +1,53 @@
+#!/usr/bin/env bash
+#
+# Multi-platform build script
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+PRG="$(basename "$0")"
+
+
+# diagnostics
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG TARGET"
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+# command line args
+
+[ "$#" -eq 0 ] && usage
+TARGET="$1"; shift
+
+[ "$#" -eq 0 ] || usage
+
+
+# main
+
+mkdir -p "$TARGET"
+
+case "$TARGET" in
+ x86_64-linux | x86_64-darwin)
+ cc -m64 exec_process.c -o "$TARGET/exec_process"
+ ;;
+ x86-linux | x86-darwin)
+ cc -m32 exec_process.c -o "$TARGET/exec_process"
+ ;;
+ x86-cygwin)
+ cc exec_process.c -o "$TARGET/exec_process.exe"
+ ;;
+ *)
+ cc exec_process.c -o "$TARGET/exec_process"
+ ;;
+esac
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/exec_process/etc/settings Wed Sep 19 18:01:48 2012 +0200
@@ -0,0 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
+EXEC_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/exec_process"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/exec_process/exec_process.c Wed Sep 19 18:01:48 2012 +0200
@@ -0,0 +1,57 @@
+/* Author: Makarius
+
+Bash process group invocation.
+*/
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <sys/types.h>
+#include <unistd.h>
+
+
+static void fail(const char *msg)
+{
+ fprintf(stderr, "%s\n", msg);
+ exit(2);
+}
+
+
+int main(int argc, char *argv[])
+{
+ /* args */
+
+ if (argc != 3) {
+ fprintf(stderr, "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;
+
+ execv("/bin/bash", cmd_line);
+ fail("Cannot exec process");
+}
+