diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-06-15 14:48:34 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-17 18:16:11 +0200 |
commit | a8088f565da008d3b1780f38de0ee894e8fd0baa (patch) | |
tree | f03b8d5eb42e69dab608cc6a30a2953283f86fbd /lib/loc.mli | |
parent | 42cbdfccf0c0500935d619dccaa00476690229f8 (diff) |
Set required version of camlp5 to 6.06.
It is already very old (shipped with Debian oldstable) and adds file name
support in locations.
Diffstat (limited to 'lib/loc.mli')
0 files changed, 0 insertions, 0 deletions