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 /checker/checker.ml | |
| parent | c1c488d08857636381d6cbf3a9202e7123923dd0 (diff) | |
fix bug 3683 : adds references to the web site for the bug tracker
in error messages
Diffstat (limited to 'checker/checker.ml')
| -rw-r--r-- | checker/checker.ml | 3 |
1 files changed, 2 insertions, 1 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 "\"" |