# HG changeset patch
# User wenzelm
# Date 1265570498 -3600
# Node ID 16f9877abf0bf13536d7cee1d0deb7091e537091
# Parent  c844b93dd147eeaf17aca7130aacf5b1b9a35786
modernized perl scripts: prefer standalone executables;
exec bash wrapper script directly -- avoid intermediate process;

diff -r c844b93dd147 -r 16f9877abf0b lib/scripts/bash
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/bash	Sun Feb 07 20:21:38 2010 +0100
@@ -0,0 +1,32 @@
+#!/usr/bin/env perl
+#
+# Author: Makarius
+#
+# bash - invoke shell command line (with robust signal handling)
+#
+
+use warnings;
+use strict;
+
+
+# args
+
+my ($group, $script_name, $pid_name, $output_name) = @ARGV;
+
+
+# process id
+
+if ($group eq "group") {
+  use POSIX "setsid";
+  POSIX::setsid || die $!;
+}
+
+open (PID_FILE, ">", $pid_name) || die $!;
+print PID_FILE "$$";
+close PID_FILE;
+
+
+# exec script
+
+$SIG{'INT'} = "DEFAULT";   #paranoia setting, required for Cygwin
+exec qq/exec bash '$script_name' > '$output_name'/;
diff -r c844b93dd147 -r 16f9877abf0b lib/scripts/system.pl
--- a/lib/scripts/system.pl	Sun Feb 07 19:54:12 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-#
-# Author: Makarius
-#
-# system.pl - invoke shell command line (with robust signal handling)
-#
-
-# args
-
-($group, $script_name, $pid_name, $output_name) = @ARGV;
-
-
-# process id
-
-if ($group eq "group") {
-  use POSIX "setsid";
-  POSIX::setsid || die $!;
-}
-
-open (PID_FILE, ">", $pid_name) || die $!;
-print PID_FILE "$$";
-close PID_FILE;
-
-
-# exec script
-
-$SIG{'INT'} = "DEFAULT";   #paranoia setting, required for Cygwin
-exec qq/exec bash '$script_name' > '$output_name'/;
-
diff -r c844b93dd147 -r 16f9877abf0b src/Pure/ML-Systems/bash.ML
--- a/src/Pure/ML-Systems/bash.ML	Sun Feb 07 19:54:12 2010 +0100
+++ b/src/Pure/ML-Systems/bash.ML	Sun Feb 07 20:21:38 2010 +0100
@@ -25,7 +25,7 @@
     val output_name = OS.FileSys.tmpName ();
 
     val status =
-      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
+      OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" nogroup " ^
         script_name ^ " /dev/null " ^ output_name);
     val rc =
       (case Posix.Process.fromStatus status of
diff -r c844b93dd147 -r 16f9877abf0b src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Feb 07 19:54:12 2010 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sun Feb 07 20:21:38 2010 +0100
@@ -180,7 +180,7 @@
     val system_thread = Thread.fork (fn () =>
       let
         val status =
-          OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" group " ^
+          OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/bash\" group " ^
             script_name ^ " " ^ pid_name ^ " " ^ output_name);
         val res =
           (case Posix.Process.fromStatus status of
diff -r c844b93dd147 -r 16f9877abf0b src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Feb 07 19:54:12 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Feb 07 20:21:38 2010 +0100
@@ -170,8 +170,7 @@
 
           Standard_System.write_file(script_file, script)
 
-          val proc = execute(true, "perl", "-w",
-            expand_path("$ISABELLE_HOME/lib/scripts/system.pl"), "group",
+          val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/bash"), "group",
             script_file.getPath, pid_file.getPath, output_file.getPath)
 
           def kill(strict: Boolean) =