src/HOL/Tools/ATP/scripts/remote_atp
changeset 38094 d01b8119b2e0
parent 38065 9069e1ad1527
child 39152 f09b378cb252
equal deleted inserted replaced
38093:ff1d4078fe9a 38094:d01b8119b2e0
    96 
    96 
    97 #catch errors / failure
    97 #catch errors / failure
    98 if(!$Response->is_success) {
    98 if(!$Response->is_success) {
    99   my $message = $Response->message;
    99   my $message = $Response->message;
   100   $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
   100   $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
   101   print $message . "\n";
   101   print "HTTP error: " . $message . "\n";
   102   exit(-1);
   102   exit(-1);
   103 } elsif (exists($Options{'w'})) {
   103 } elsif (exists($Options{'w'})) {
   104   print $Response->content;
   104   print $Response->content;
   105   exit (0);
   105   exit (0);
   106 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
   106 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {