diff options
| author | Emilio Jesus Gallego Arias | 2020-03-30 18:58:24 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:17:16 -0400 |
| commit | 7afd5e9fb7ba9e5fc41e41fd54eb90ee8cb13993 (patch) | |
| tree | 1d8ee10d5c7a8f38d79863ca4a99e5d83e612aee /plugins | |
| parent | 0eadf776ba78dcfdcab842f38f5de871ed337376 (diff) | |
[proof] Improve comment and argument name.
As suggested by Gaëtan Gilbert.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions