changeset 41522 | 42d13d00ccfb |
parent 41491 | a2ad5b824051 |
child 43074 | 8b566f0d226c |
--- a/src/Tools/WWW_Find/scgi_server.ML Wed Jan 12 15:09:26 2011 +0100 +++ b/src/Tools/WWW_Find/scgi_server.ML Wed Jan 12 15:15:51 2011 +0100 @@ -89,7 +89,7 @@ else f (req, get_content content_is, send))) end; - fun thread_req () = + fun thread_req () = (* FIXME avoid handle e *) (do_req () handle e => (warning (exnMessage e)); BinIO.closeOut sout handle e => warning (exnMessage e); BinIO.closeIn sin handle e => warning (exnMessage e);