diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 15:36:33 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:17:16 -0400 |
| commit | 7a2e41abd8559d0bd4683e513dcb0b83987a9128 (patch) | |
| tree | 0a281380929879825b694d97770d07de6220a0ae /plugins/syntax/plugin_base.dune | |
| parent | 49b559ccb6d17b5356bc0e43c81a8363ec0b4768 (diff) | |
[proof] Remove unused parameter in the delayed save path.
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions