clarified command-line;
authorwenzelm
Thu, 22 Apr 2021 22:07:05 +0200
changeset 73855 981df2e1f646
parent 73854 461da479f95c
child 73856 328392479308
clarified command-line;
Admin/bash_process/bash_process.c
Admin/bash_process/build
Admin/bash_process/etc/settings
Admin/components/components.sha1
Admin/components/main
src/Pure/System/bash.scala
--- a/Admin/bash_process/bash_process.c	Thu Apr 22 22:04:54 2021 +0200
+++ b/Admin/bash_process/bash_process.c	Thu Apr 22 22:07:05 2021 +0200
@@ -37,13 +37,12 @@
 {
   /* args */
 
-  if (argc < 3) {
-    fprintf(stderr, "Bad arguments: PID_FILE and TIMING_FILE required\n");
+  if (argc < 2) {
+    fprintf(stderr, "Bad arguments: missing TIMING_FILE\n");
     fflush(stderr);
     exit(1);
   }
-  char *pid_name = argv[1];
-  char *timing_name = argv[2];
+  char *timing_name = argv[1];
 
 
   /* potential fork */
@@ -101,26 +100,16 @@
 
   /* 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);
-  }
+  fprintf(stdout, "%d\n", getpid());
+  fflush(stdout);
 
 
   /* shift command line */
 
   int i;
-  for (i = 3; i < argc; i++) {
-    argv[i - 3] = argv[i];
+  for (i = 2; i < argc; i++) {
+    argv[i - 2] = argv[i];
   }
-  argv[argc - 3] = NULL;
   argv[argc - 2] = NULL;
   argv[argc - 1] = NULL;
 
--- a/Admin/bash_process/build	Thu Apr 22 22:04:54 2021 +0200
+++ b/Admin/bash_process/build	Thu Apr 22 22:07:05 2021 +0200
@@ -36,16 +36,16 @@
 mkdir -p "$TARGET"
 
 case "$TARGET" in
+  arm64-linux)
+    cc -Wall bash_process.c -o "$TARGET/bash_process"
+    ;;
   x86_64-linux | x86_64-darwin)
     cc -Wall -m64 bash_process.c -o "$TARGET/bash_process"
     ;;
-  x86-linux | x86-darwin)
-    cc -Wall -m32 bash_process.c -o "$TARGET/bash_process"
-    ;;
-  x86_64-cygwin | x86-cygwin)
+  x86_64-cygwin)
     cc -Wall bash_process.c -o "$TARGET/bash_process.exe"
     ;;
   *)
-    cc -Wall bash_process.c -o "$TARGET/bash_process"
+    fail "Bad target platform: \"$TARGET\""
     ;;
 esac
--- a/Admin/bash_process/etc/settings	Thu Apr 22 22:04:54 2021 +0200
+++ b/Admin/bash_process/etc/settings	Thu Apr 22 22:07:05 2021 +0200
@@ -1,3 +1,3 @@
 # -*- shell-script -*- :mode=shellscript:
 
-ISABELLE_BASH_PROCESS="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bash_process"
+ISABELLE_BASH_PROCESS="$COMPONENT/$ISABELLE_PLATFORM64/bash_process"
--- a/Admin/components/components.sha1	Thu Apr 22 22:04:54 2021 +0200
+++ b/Admin/components/components.sha1	Thu Apr 22 22:07:05 2021 +0200
@@ -13,6 +13,7 @@
 97b2491382130a841b3bbaebdcf8720c4d4fb227  bash_process-1.2.2.tar.gz
 5c5b7c18cc1dc2a4d22b997dac196da09eaca868  bash_process-1.2.3-1.tar.gz
 48b01bd9436e243ffcb7297f08b498d0c0875ed9  bash_process-1.2.3.tar.gz
+7ae9ec8aab2d8a811842d9dc67d8bf6c179e11ee  bash_process-1.2.4.tar.gz
 9e21f447bfa0431ae5097301d553dd6df3c58218  bash_process-1.2.tar.gz
 a65ce644b6094d41e9f991ef851cf05eff5dd0a9  bib2xhtml-20171221.tar.gz
 4085dd6060a32d7e0d2e3f874c463a9964fd409b  bib2xhtml-20190409.tar.gz
--- a/Admin/components/main	Thu Apr 22 22:04:54 2021 +0200
+++ b/Admin/components/main	Thu Apr 22 22:07:05 2021 +0200
@@ -1,6 +1,6 @@
 #main components for everyday use, without big impact on overall build time
 gnu-utils-20210414
-bash_process-1.2.3-1
+bash_process-1.2.4
 bib2xhtml-20190409
 csdp-6.1.1
 cvc4-1.8
--- a/src/Pure/System/bash.scala	Thu Apr 22 22:04:54 2021 +0200
+++ b/src/Pure/System/bash.scala	Thu Apr 22 22:07:05 2021 +0200
@@ -70,7 +70,7 @@
 
     private val proc =
       Isabelle_System.process(
-        List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
+        List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
           File.standard_path(timing_file), "bash", File.standard_path(script_file)),
         cwd = cwd, env = env, redirect = redirect)