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

--- a/src/HOL/Tools/ATP_Manager/lib/scripts/local_atp.pl	Tue Sep 15 15:29:11 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-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";
-}