aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.install
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-09 01:09:00 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-03-10 16:21:24 +0100
commitccb706774a8f9bf4f58f6899a58e6cc5117901a6 (patch)
tree109928757371fc52805147b2404daf3af859b17e /Makefile.install
parent7812c5f39dd166559847c1ece573b02653e62100 (diff)
[META] Ltac now a plugin.
Diffstat (limited to 'Makefile.install')
0 files changed, 0 insertions, 0 deletions