diff options
| author | Maxime Dénès | 2017-12-27 10:19:13 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-27 10:19:13 +0100 |
| commit | 3921ff2e2c189063ec46f54cbb247570b6c59b2c (patch) | |
| tree | f4f6949c303bfdf539f0947e5516c8b552a8ce2a /plugins | |
| parent | c139ae10fef08c021ae718719ba49b86a8d88cf3 (diff) | |
| parent | 315fb733dd2e7827b3f3ea8a07b725b2a46519ff (diff) | |
Merge PR #6443: [vernac] Cleanup of do_definition.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions