diff options
| author | Gaëtan Gilbert | 2020-02-20 16:31:53 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-31 14:39:43 +0200 |
| commit | f19cf4259f63a9c0392c922527e0e9002192949e (patch) | |
| tree | 5f0cf9440e877bf8f1e6b94c13776b8e4060da1d /plugins/syntax/plugin_base.dune | |
| parent | c0a71f9ff6289d99bbbcd13ef65c68f74ac9e191 (diff) | |
Remove check_hidden_implicit_parameters (not needed anymore)
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions