diff -r e332b08bf0f3 -r 24090eae50b6 src/Tools/WWW_Find/http_status.ML --- a/src/Tools/WWW_Find/http_status.ML Fri Nov 20 15:48:36 2009 +0100 +++ b/src/Tools/WWW_Find/http_status.ML Fri Nov 20 16:08:14 2009 +0100 @@ -1,8 +1,9 @@ -(* Title: http_status.ML +(* Title: Tools/WWW_Find/http_status.ML Author: Timothy Bourke, NICTA HTTP status codes and reasons. *) + signature HTTP_STATUS = sig type t