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 /lib/pp.ml | |
parent | c1c488d08857636381d6cbf3a9202e7123923dd0 (diff) |
fix bug 3683 : adds references to the web site for the bug tracker
in error messages
Diffstat (limited to 'lib/pp.ml')
0 files changed, 0 insertions, 0 deletions