diff options
| author | Emilio Jesus Gallego Arias | 2019-12-13 17:43:33 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-12-24 13:18:02 +0100 |
| commit | 8ca6ef52ae0091a694b1047ca1ca53d7d836a3a3 (patch) | |
| tree | 2a6b9d45182d2d9eb1af3f9f3dbaa288111f0528 /plugins | |
| parent | 23eb6e3805738ad244f37e73c34e0488dc9c71f8 (diff) | |
[meta] Add ltac2 information to META.
Closes #11225 , we use a bit of a hack due to the way the Makefile
installs this plugin.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions