aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.ml
diff options
context:
space:
mode:
authorGravatar Yves Bertot <yves.bertot@inria.fr>2016-09-28 16:24:51 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-29 15:55:39 +0200
commit6d20e4c136fb2726ec8577bdfee051ecacdf8261 (patch)
tree61253d2ab100bffaf6971516050290263cc44bae /lib/pp.ml
parentc1c488d08857636381d6cbf3a9202e7123923dd0 (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