diff options
| author | Maxime Dénès | 2019-07-25 15:42:30 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-30 12:17:12 +0100 |
| commit | b76db7671bc23238938bc090af0e00b3009f481c (patch) | |
| tree | cade05050f9bd7fbe9d3c39feb8ad8b08fc0cb6b /plugins | |
| parent | 639886e771882e2c3302cbadc35e9383b34db1fe (diff) | |
Deprecation annotation for `convert_concl_no_check`
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions