diff options
| author |  Théo Winterhalter <isheeft@gmail.com> | 2018-05-31 10:58:39 +0200 |
|---|---|---|
| committer | Théo Winterhalter <isheeft@gmail.com> | 2018-05-31 10:58:39 +0200 |
| commit | 1967ddb1fb4eb250b2bb10c9f8fbdc56fa954fe1 (patch) | |
| tree | 04048656348d6786e7e8003fff52bf8113b32e2c /plugins/ltac/extraargs.mli | |
| parent | 4598a26890a896ddcf6cd30758ae07882e245a16 (diff) | |
Indicate in the doc that clearbody can take several idents
Diffstat (limited to 'plugins/ltac/extraargs.mli')
0 files changed, 0 insertions, 0 deletions