From 6d20e4c136fb2726ec8577bdfee051ecacdf8261 Mon Sep 17 00:00:00 2001
From: Yves Bertot <yves.bertot@inria.fr>
Date: Wed, 28 Sep 2016 16:24:51 +0200
Subject: fix bug 3683 : adds references to the web site for the bug tracker in
 error messages

---
 lib/cErrors.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'lib/cErrors.ml')

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 1459141d1..c69c7e400 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -93,7 +93,9 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
+    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++
+           strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
+           str ".")
   else
     hov 0 (raw_anomaly e)
 
-- 
cgit v1.2.3