# HG changeset patch
# User wenzelm
# Date 1288085482 -7200
# Node ID 51e026049e4d686d6ab697887d1b1a7c2b7b8897
# Parent  752a26dce4bea78413c51cd350f24521e72f4827
do not handle arbitrary exceptions;

diff -r 752a26dce4be -r 51e026049e4d src/Tools/WWW_Find/scgi_req.ML
--- a/src/Tools/WWW_Find/scgi_req.ML	Tue Oct 26 11:23:27 2010 +0200
+++ b/src/Tools/WWW_Find/scgi_req.ML	Tue Oct 26 11:31:22 2010 +0200
@@ -106,8 +106,9 @@
        | SOME wv => Byte.unpackStringVec wv);
 
     val content_length =
-      (the o Int.fromString o field) "CONTENT_LENGTH"
-      handle _ => raise InvalidReq "Bad CONTENT_LENGTH";
+      (case Int.fromString (field "CONTENT_LENGTH") of
+        SOME n => n
+      | NONE => raise InvalidReq "Bad CONTENT_LENGTH");
 
     val req = Req {
         path_info = field "PATH_INFO",