src/HOL/Tools/ATP/scripts/remote_atp

--- a/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 19:03:46 2010 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp	Thu Jul 29 19:26:42 2010 +0200
@@ -98,7 +98,7 @@
 if(!$Response->is_success) {
   my $message = $Response->message;
   $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
-  print $message . "\n";
+  print "HTTP error: " . $message . "\n";
   exit(-1);
 } elsif (exists($Options{'w'})) {
   print $Response->content;