aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-04 16:18:06 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-04 16:18:06 +0200
commitda99355b4d6de31aec5a660f7afe100190a8e683 (patch)
tree3b00f4b967ad27eb90518627948275fb0b7b72d2 /Makefile.build
parentc78b84425be7535e46c63e80200c07a1921e67bd (diff)
Revert "Revert "Improve the interpretation scope of arguments of an ltac match.""
We apply this patch to trunk so that it is integrated in 8.6. This reverts commit 0eb08b70f0c576e58912c1fc3ef74f387ad465be.
Diffstat (limited to 'Makefile.build')
0 files changed, 0 insertions, 0 deletions