changeset 41491 | a2ad5b824051 |
parent 33823 | 24090eae50b6 |
child 43278 | 1fbdcebb364b |
--- a/src/Tools/WWW_Find/http_util.ML Mon Jan 10 15:30:17 2011 +0100 +++ b/src/Tools/WWW_Find/http_util.ML Mon Jan 10 15:45:46 2011 +0100 @@ -21,7 +21,7 @@ fun reply_header (status, content_type, extra_fields) = let - val code = (Int.toString o HttpStatus.to_status_code) status; + val code = (string_of_int o HttpStatus.to_status_code) status; val reason = HttpStatus.to_reason status; val show_content_type = pair "Content-Type" o Mime.show_type; in