diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-09 01:09:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-10 16:21:24 +0100 |
| commit | ccb706774a8f9bf4f58f6899a58e6cc5117901a6 (patch) | |
| tree | 109928757371fc52805147b2404daf3af859b17e /configure.ml | |
| parent | 7812c5f39dd166559847c1ece573b02653e62100 (diff) | |
[META] Ltac now a plugin.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions