--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/bash_process/bash_process.c Sat Feb 13 17:27:23 2016 +0100
@@ -0,0 +1,72 @@
+/* Author: Makarius
+
+Bash process with separate process group id.
+*/
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <sys/types.h>
+#include <unistd.h>
+
+
+static void fail(const char *msg)
+{
+ fprintf(stderr, "%s\n", msg);
+ fflush(stderr);
+ exit(2);
+}
+
+
+int main(int argc, char *argv[])
+{
+ /* args */
+
+ if (argc < 2) {
+ fprintf(stderr, "Bad arguments: missing pid file\n");
+ fflush(stderr);
+ exit(1);
+ }
+ char *pid_name = argv[1];
+
+
+ /* 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)");
+ }
+
+
+ /* report pid */
+
+ if (strcmp(pid_name, "-") == 0) {
+ fprintf(stdout, "%d\n", getpid());
+ fflush(stdout);
+ }
+ else if (strlen(pid_name) > 0) {
+ 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);
+ }
+
+
+ /* shift command line */
+
+ int i;
+ for (i = 2; i < argc; i++) {
+ argv[i - 2] = argv[i];
+ }
+ argv[argc - 2] = NULL;
+ argv[argc - 1] = NULL;
+
+
+ /* exec */
+
+ execvp("bash", argv);
+ fail("Cannot exec process");
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/bash_process/build Sat Feb 13 17:27:23 2016 +0100
@@ -0,0 +1,51 @@
+#!/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 bash_process.c -o "$TARGET/bash_process"
+ ;;
+ x86-linux | x86-darwin)
+ cc -m32 bash_process.c -o "$TARGET/bash_process"
+ ;;
+ x86-cygwin)
+ cc bash_process.c -o "$TARGET/bash_process.exe"
+ ;;
+ *)
+ cc bash_process.c -o "$TARGET/bash_process"
+ ;;
+esac
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/bash_process/etc/settings Sat Feb 13 17:27:23 2016 +0100
@@ -0,0 +1,3 @@
+# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_BASH_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bash_process"
--- a/Admin/exec_process/build Sat Feb 13 17:24:00 2016 +0100
+++ /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/exec_process/etc/settings Sat Feb 13 17:24:00 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-EXEC_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/exec_process"
--- a/Admin/exec_process/exec_process.c Sat Feb 13 17:24:00 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-/* Author: Makarius
-
-Bash process with separate process group id.
-*/
-
-#include <stdlib.h>
-#include <stdio.h>
-#include <string.h>
-#include <sys/types.h>
-#include <unistd.h>
-
-
-static void fail(const char *msg)
-{
- fprintf(stderr, "%s\n", msg);
- fflush(stderr);
- exit(2);
-}
-
-
-int main(int argc, char *argv[])
-{
- /* args */
-
- if (argc < 2) {
- fprintf(stderr, "Bad arguments: missing pid file\n");
- fflush(stderr);
- exit(1);
- }
- char *pid_name = argv[1];
-
-
- /* 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)");
- }
-
-
- /* report pid */
-
- if (strcmp(pid_name, "-") == 0) {
- fprintf(stdout, "%d\n", getpid());
- fflush(stdout);
- }
- else if (strlen(pid_name) > 0) {
- 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);
- }
-
-
- /* shift command line */
-
- int i;
- for (i = 2; i < argc; i++) {
- argv[i - 2] = argv[i];
- }
- argv[argc - 2] = NULL;
- argv[argc - 1] = NULL;
-
-
- /* exec */
-
- execvp("bash", argv);
- fail("Cannot exec process");
-}