diff options
| author | Hendrik Tews | 2021-03-29 11:03:50 +0200 |
|---|---|---|
| committer | Hendrik Tews | 2021-04-12 20:56:40 +0200 |
| commit | ad34e3a7703d326268bab203864aa84ad3718c2c (patch) | |
| tree | ab2fdc8d9ff49b5da8c2ea4f22d7ddc8367fce9f /dev | |
| parent | 1947e54a2331dbbb8cd0f46b40bbb1524a67df54 (diff) | |
Fix unknown -vos option for coqdep_boot introduced in PR #11074
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions