diff -r e332b08bf0f3 -r 24090eae50b6 src/Tools/WWW_Find/scgi_server.ML --- a/src/Tools/WWW_Find/scgi_server.ML Fri Nov 20 15:48:36 2009 +0100 +++ b/src/Tools/WWW_Find/scgi_server.ML Fri Nov 20 16:08:14 2009 +0100 @@ -1,4 +1,4 @@ -(* Title: scgi_echo.ML +(* Title: Tools/WWW_Find/scgi_server.ML Author: Timothy Bourke, NICTA Simple SCGI server.