From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 24 Jan 2005 12:57:00 +0000 (+0000)
Subject: added helm:exception handling of Http_getter_types.Key_not_found
X-Git-Tag: V_0_1_0~98
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=829bcae5f3b90741d2e747520842a54e55e8c779;p=helm.git

added helm:exception handling of Http_getter_types.Key_not_found
---

diff --git a/helm/http_getter/main.ml b/helm/http_getter/main.ml
index f65e991b7..b2a75488a 100644
--- a/helm/http_getter/main.ml
+++ b/helm/http_getter/main.ml
@@ -336,8 +336,12 @@ let callback (req: Http_types.request) outchan =
         (String.concat "<br />\n" msgs) outchan
   | exc ->
       let msg = "Uncaught exception: " ^ (Printexc.to_string exc) in
-      log_failure msg;
-      return_html_error "Uncaught_exception" msg outchan
+      (match exc with
+      | Http_getter_types.Key_not_found uri ->
+          return_html_error "Key_not_found" msg outchan
+      | _ ->
+          log_failure msg;
+          return_html_error "Uncaught_exception" msg outchan)
 
     (* Main *)