diff options
| author | Hugo Herbelin | 2019-05-10 09:36:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 02:31:27 +0200 |
| commit | f2779d48d3b7735687444e22b16cdb7cb8f7ce60 (patch) | |
| tree | 5c17149292f54e3bfe3b4d3977825a10c3de8a92 /plugins/syntax/plugin_base.dune | |
| parent | fe487e8eaae3186803ec657c517d0ebebab3bafd (diff) | |
Usage: bypassing a useless detour via a reference.
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions