src/Tools/WWW_Find/scgi_server.ML
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);