diff options
| author | Emilio Jesus Gallego Arias | 2019-10-31 03:48:21 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-12 20:36:27 -0400 |
| commit | e8797829a459d27975af57f88e7d4110da4fa009 (patch) | |
| tree | 633b08b3f19b8100e1ce1333e62b22db36055059 /plugins/syntax/plugin_base.dune | |
| parent | 76d8a38a4591c604795c5429ffcbbe9daaa8945d (diff) | |
[vernac] Minor cleanup of opens in `Vernacentries`
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions