# HG changeset patch # User wenzelm # Date 1619122025 -7200 # Node ID 981df2e1f646daa630b0d78e58205614116e91aa # Parent 461da479f95c8f15f58e06f959757b2000674325 clarified command-line; diff -r 461da479f95c -r 981df2e1f646 Admin/bash_process/bash_process.c --- 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; diff -r 461da479f95c -r 981df2e1f646 Admin/bash_process/build --- 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 diff -r 461da479f95c -r 981df2e1f646 Admin/bash_process/etc/settings --- 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" diff -r 461da479f95c -r 981df2e1f646 Admin/components/components.sha1 --- 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 diff -r 461da479f95c -r 981df2e1f646 Admin/components/main --- 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 diff -r 461da479f95c -r 981df2e1f646 src/Pure/System/bash.scala --- 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)