| changeset 40684 | c7ba327eb58c |
| parent 36898 | 8e55aa1306c5 |
| child 41432 | 3214c39777ab |
--- a/src/HOL/Tools/SMT/lib/scripts/remote_smt Wed Nov 24 10:52:02 2010 +0100 +++ b/src/HOL/Tools/SMT/lib/scripts/remote_smt Wed Nov 24 16:15:15 2010 +0100 @@ -26,6 +26,6 @@ "Options" => join(" ", @options), "Problem" => [$problem_file] ], "Content_Type" => "form-data"); -if (not $response->is_success) { die "HTTP-Error: " . $response->message; } +if (not $response->is_success) { die "HTTP error: " . $response->message; } else { print $response->content; }