diff options
| author | Emilio Jesus Gallego Arias | 2019-10-30 17:55:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-25 15:34:22 -0500 |
| commit | fda9bdb09a2f2f7b98351e047ae43f097b428902 (patch) | |
| tree | bd42dbec8e24093b071db676b66188aca0424da6 /plugins/syntax/plugin_base.dune | |
| parent | fe1335eb350c305142bf4be57c681891515a5dac (diff) | |
[vernac] Remove deprecated function.
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions