1.1 --- a/Admin/Cygwin/exec_process.c	Fri Apr 27 19:31:03 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,57 +0,0 @@
     1.4 -/*  Author:     Makarius
     1.5 -
     1.6 -Bash process group invocation on Cygwin.
     1.7 -*/
     1.8 -
     1.9 -#include <stdlib.h>
    1.10 -#include <stdio.h>
    1.11 -#include <sys/types.h>
    1.12 -#include <unistd.h>
    1.13 -
    1.14 -
    1.15 -static void fail(const char *msg)
    1.16 -{
    1.17 -  printf("%s\n", msg);
    1.18 -  exit(2);
    1.19 -}
    1.20 -
    1.21 -
    1.22 -int main(int argc, char *argv[])
    1.23 -{
    1.24 -  /* args */
    1.25 -
    1.26 -  if (argc != 3) {
    1.27 -    printf("Bad arguments\n");
    1.28 -    exit(1);
    1.29 -  }
    1.30 -  char *pid_name = argv[1];
    1.31 -  char *script = argv[2];
    1.32 -
    1.33 -
    1.34 -  /* report pid */
    1.35 -
    1.36 -  FILE *pid_file;
    1.37 -  pid_file = fopen(pid_name, "w");
    1.38 -  if (pid_file == NULL) fail("Cannot open pid file");
    1.39 -  fprintf(pid_file, "%d", getpid());
    1.40 -  fclose(pid_file);
    1.41 -
    1.42 -
    1.43 -  /* setsid */
    1.44 -
    1.45 -  if (getgid() == getpid()) fail("Cannot set session id");
    1.46 -  setsid();
    1.47 -
    1.48 -
    1.49 -  /* exec */
    1.50 -
    1.51 -  char *cmd_line[4];
    1.52 -  cmd_line[0] = "/bin/bash";
    1.53 -  cmd_line[1] = "-c";
    1.54 -  cmd_line[2] = script;
    1.55 -  cmd_line[3] = NULL;
    1.56 -
    1.57 -  execv("/bin/bash", cmd_line);
    1.58 -  fail("Cannot exec process");
    1.59 -}
    1.60 -

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/Admin/exec_process/exec_process.c	Fri Apr 27 19:50:32 2012 +0200
     2.3 @@ -0,0 +1,57 @@
     2.4 +/*  Author:     Makarius
     2.5 +
     2.6 +Bash process group invocation.
     2.7 +*/
     2.8 +
     2.9 +#include <stdlib.h>
    2.10 +#include <stdio.h>
    2.11 +#include <sys/types.h>
    2.12 +#include <unistd.h>
    2.13 +
    2.14 +
    2.15 +static void fail(const char *msg)
    2.16 +{
    2.17 +  printf("%s\n", msg);
    2.18 +  exit(2);
    2.19 +}
    2.20 +
    2.21 +
    2.22 +int main(int argc, char *argv[])
    2.23 +{
    2.24 +  /* args */
    2.25 +
    2.26 +  if (argc != 3) {
    2.27 +    printf("Bad arguments\n");
    2.28 +    exit(1);
    2.29 +  }
    2.30 +  char *pid_name = argv[1];
    2.31 +  char *script = argv[2];
    2.32 +
    2.33 +
    2.34 +  /* report pid */
    2.35 +
    2.36 +  FILE *pid_file;
    2.37 +  pid_file = fopen(pid_name, "w");
    2.38 +  if (pid_file == NULL) fail("Cannot open pid file");
    2.39 +  fprintf(pid_file, "%d", getpid());
    2.40 +  fclose(pid_file);
    2.41 +
    2.42 +
    2.43 +  /* setsid */
    2.44 +
    2.45 +  if (getgid() == getpid()) fail("Cannot set session id");
    2.46 +  setsid();
    2.47 +
    2.48 +
    2.49 +  /* exec */
    2.50 +
    2.51 +  char *cmd_line[4];
    2.52 +  cmd_line[0] = "/bin/bash";
    2.53 +  cmd_line[1] = "-c";
    2.54 +  cmd_line[2] = script;
    2.55 +  cmd_line[3] = NULL;
    2.56 +
    2.57 +  execv("/bin/bash", cmd_line);
    2.58 +  fail("Cannot exec process");
    2.59 +}
    2.60 +

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/Admin/exec_process/mk	Fri Apr 27 19:50:32 2012 +0200
     3.3 @@ -0,0 +1,3 @@
     3.4 +#!/bin/bash
     3.5 +
     3.6 +cc exec_process.c -o exec_process