aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.install
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-22 19:31:18 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-22 19:34:01 +0100
commit947d93a8b7ff0fc7ba23633fcd44820427e29326 (patch)
tree8257bdccc135ec71108ebfa1fc212951c9271abf /Makefile.install
parent8b73fd7c6ce423f8c8a2594e90200f2407795d52 (diff)
Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.
This adds at least support for camlp5 6.14 (in addition to 6.17).
Diffstat (limited to 'Makefile.install')
0 files changed, 0 insertions, 0 deletions