src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl	Tue Sep 15 15:29:11 2009 +0200
@@ -0,0 +1,15 @@
+use POSIX qw(setsid);
+
+$SIG{'INT'} = "DEFAULT";
+
+defined (my $pid = fork) or die "$!";
+if (not $pid) {
+  POSIX::setsid or die $!;
+  exec @ARGV;
+}
+else {
+  wait;
+  my ($user, $system, $cuser, $csystem) = times;
+  my $time = ($user + $cuser) * 1000;
+  print "$time\n";
+}