diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-27 15:13:00 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-27 15:13:00 +0200 |
| commit | 6c1de7bcc111390400b0791cc910c86d9060333b (patch) | |
| tree | 205e968e203f9cb0d2e1499c6d88d923190e8771 /lib/cErrors.ml | |
| parent | 0b218382841f56408558a09bc7de823319ac8772 (diff) | |
| parent | 89fc40027cd083ea26b58b135ede487f665bc7b9 (diff) | |
Merge remote-tracking branch 'github/pr/290' into trunk
Was PR#290: Add a compatibility flag for 8.6 and refactor.
Diffstat (limited to 'lib/cErrors.ml')
0 files changed, 0 insertions, 0 deletions