# HG changeset patch
# User blanchet
# Date 1308820781 -7200
# Node ID 35f74aafc87872e56d61a86e55a9b4b6e62e20e4
# Parent  2b92a6943915c3d63ae94520b7e0ca3e08d8c061
give slightly more time to server to respond, to avoid leaving too much garbage on Geoff's servers

diff -r 2b92a6943915 -r 35f74aafc878 src/HOL/Tools/ATP/scripts/remote_atp
--- a/src/HOL/Tools/ATP/scripts/remote_atp	Wed Jun 22 15:58:55 2011 -0700
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jun 23 11:19:41 2011 +0200
@@ -94,7 +94,7 @@
 $Agent->env_proxy;
 if (exists($Options{'t'})) {
   # give server more time to respond
-  $Agent->timeout($Options{'t'} + 10);
+  $Agent->timeout($Options{'t'} + 15);
 }
 my $Request = POST($SystemOnTPTPFormReplyURL,
 	Content_Type => 'form-data',Content => \%URLParameters);