diff options
| author | Pierre-Marie Pédrot | 2015-02-21 21:20:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-21 21:20:39 +0100 |
| commit | c193ee0750dde9184da7dca2853ad487f118cb51 (patch) | |
| tree | 229bf79223f29a02bc63a49a98ed096f75024eee /lib/errors.mli | |
| parent | 1283620790b860d91871372fb8b05dfc700c1fd9 (diff) | |
Fixing bug #3071.
Diffstat (limited to 'lib/errors.mli')
0 files changed, 0 insertions, 0 deletions