diff options
| author | Gaëtan Gilbert | 2019-11-20 15:31:57 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-21 14:31:12 +0100 |
| commit | 799bd29627c554f83c1ec9b4a226a739632cbc29 (patch) | |
| tree | 22d10310369f8be2488655785b04fd139bf22866 /plugins | |
| parent | b680b06b31c27751a7d551d95839aea38f7fbea1 (diff) | |
Document -vos flag for coqdep
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions