diff options
| author | Maxime Dénès | 2016-06-15 14:48:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 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