diff options
| author | Yves Bertot | 2016-09-28 16:24:51 +0200 |
|---|---|---|
| committer | Maxime Dénès | 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