1.1 --- a/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 00:28:57 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 09:41:49 2010 +0200
     1.3 @@ -96,13 +96,15 @@
     1.4  
     1.5  #catch errors / failure
     1.6  if(!$Response->is_success) {
     1.7 -  print "HTTP-Error: " . $Response->message . "\n";
     1.8 +  my $message = $Response->message;
     1.9 +  $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
    1.10 +  print $message . "\n";
    1.11    exit(-1);
    1.12  } elsif (exists($Options{'w'})) {
    1.13    print $Response->content;
    1.14    exit (0);
    1.15  } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
    1.16 -  print "Specified system $1 does not exist\n";
    1.17 +  print "The ATP \"$1\" is not available at SystemOnTPTP\n";
    1.18    exit(-1);
    1.19  } else {
    1.20    print $Response->content;