diff options
| author | Enrico Tassi | 2021-01-06 17:00:18 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-26 15:27:22 +0100 |
| commit | 028342741eee445c44db2661b1c246623c96e01a (patch) | |
| tree | 4ae607617fbc405486927de19114f831b215db12 /Makefile.dev | |
| parent | df3cbbee21cfaf03f7c2b9bd78280f25a5512f5a (diff) | |
[coqargs] use option injection for -w
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions