]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 828ef0c)
pretty print errors using red color instead of h1 text (close #50)
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 25 Mar 2003 15:49:08 +0000 (15:49 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 25 Mar 2003 15:49:08 +0000 (15:49 +0000)
helm/uwobo/uwobo_common.ml patch | blob | history

diff --git a/helm/uwobo/uwobo_common.ml b/helm/uwobo/uwobo_common.ml
index 5578b09fbc85a0fc016c4004f7340dc84acf0597..c71024ce8c40427dae4804cf209c2af03fd58a0d 100644 (file)
--- a/helm/uwobo/uwobo_common.ml
+++ b/helm/uwobo/uwobo_common.ml
@@ -109,11 +109,12 @@ let usage_string =
   (String.concat ", " supported_properties) (* supported properties *)
 ;;
 
-let pp_error = sprintf "<html><body><h1>Error: %s</h1></body></html>";;
+let pp_error =
+  sprintf "<html><body><span style=\"color:red\">Error: %s</span></body></html>"
+;;
 let return_error msg outchan =
   Http_daemon.respond ~body:(pp_error msg) outchan;;
 let bad_request body outchan =
   Http_daemon.respond_error ~code:400 ~body outchan
 ;;
 
-
Unnamed repository; edit this file 'description' to name the repository.