diff options
| author | Gaëtan Gilbert | 2019-11-08 11:36:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-08 11:36:22 +0100 |
| commit | 6930dd3533e7829184daa4cd8a84be62d9886c77 (patch) | |
| tree | 78600ee4e921af2ebaf67dd42e9cb6594f52745c /kernel | |
| parent | 4658804c1f5d9c89f23e2c31a44643ed4569f9fe (diff) | |
coqdep: only output vos when passed -vos
This fixes dune. TBH the problem is that dune is too strict, but we
can't go back in time to change it.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions