diff options
| author |  Yves Bertot <yves.bertot@inria.fr> | 2016-09-28 16:24:51 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-29 15:55:39 +0200 |
| commit | 6d20e4c136fb2726ec8577bdfee051ecacdf8261 (patch) | |
| tree | 61253d2ab100bffaf6971516050290263cc44bae | |
| parent | c1c488d08857636381d6cbf3a9202e7123923dd0 (diff) | |
fix bug 3683 : adds references to the web site for the bug tracker
in error messages
| -rw-r--r-- | checker/checker.ml | 3 | ||||
| -rw-r--r-- | config/coq_config.mli | 1 | ||||
| -rw-r--r-- | configure.ml | 1 | ||||
| -rw-r--r-- | lib/cErrors.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 4 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 3 |
6 files changed, 12 insertions, 4 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 0c411ae44..503697b59 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -209,7 +209,8 @@ let usage () = open Type_errors let anomaly_string () = str "Anomaly: " -let report () = (str "." ++ spc () ++ str "Please report.") +let report () = (str "." ++ spc () ++ str "Please report" ++ + strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".") let guill s = str "\"" ++ str s ++ str "\"" diff --git a/config/coq_config.mli b/config/coq_config.mli index a0e1019fa..6087c0116 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -62,6 +62,7 @@ val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *) val wwwcoq : string val wwwrefman : string +val wwwbugtracker : string val wwwstdlib : string val localwwwrefman : string diff --git a/configure.ml b/configure.ml index 2c1d531ea..23ec93e07 100644 --- a/configure.ml +++ b/configure.ml @@ -1043,6 +1043,7 @@ let write_configml f = pr "let with_geoproof = ref %B\n" !Prefs.geoproof; pr_s "browser" browser; pr_s "wwwcoq" !Prefs.coqwebsite; + pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/"); pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); 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) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 0d4807e16..69d68bd35 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -348,5 +348,7 @@ let rec loop () = | any -> Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++ str (Printexc.to_string any) ++ - fnl() ++ str"Please report."); + fnl() ++ + str"Please report" ++ + strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); loop () diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ff4c18ad2..6ee695bc2 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -304,7 +304,8 @@ let explain_unification_error env sigma p1 p2 = function else [] | MetaOccurInBody evk -> [str "instance for " ++ quote (pr_existential_key sigma evk) ++ - strbrk " refers to a metavariable - please report your example"] + strbrk " refers to a metavariable - please report your example" ++ + strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."] | InstanceNotSameType (evk,env,t,u) -> let t, u = pr_explicit env sigma t u in [str "unable to find a well-typed instantiation for " ++ |