src/HOL/Tools/ATP/scripts/remote_atp
changeset 46241 1a0b8f529b96
parent 43528 35f74aafc878
child 60584 6ac3172985d4
equal deleted inserted replaced
46240:933f35c4e126 46241:1a0b8f529b96
    90 }
    90 }
    91 
    91 
    92 # Query Server
    92 # Query Server
    93 my $Agent = LWP::UserAgent->new;
    93 my $Agent = LWP::UserAgent->new;
    94 $Agent->env_proxy;
    94 $Agent->env_proxy;
       
    95 $Agent->agent("Sledgehammer");
    95 if (exists($Options{'t'})) {
    96 if (exists($Options{'t'})) {
    96   # give server more time to respond
    97   # give server more time to respond
    97   $Agent->timeout($Options{'t'} + 15);
    98   $Agent->timeout($Options{'t'} + 15);
    98 }
    99 }
    99 my $Request = POST($SystemOnTPTPFormReplyURL,
   100 my $Request = POST($SystemOnTPTPFormReplyURL,