diff options
| author | Hugo Herbelin | 2019-05-25 15:48:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-25 15:48:40 +0200 |
| commit | f6811213b24b5646404d3f3ad48a4ec79eb12dab (patch) | |
| tree | f4610628ed2af78fc80ae010be3e1904156fe4f9 /interp | |
| parent | 5727443376480be4793757fd5507621ad4f09509 (diff) | |
Coqc: Treat unknown arguments starting with dash as unknown options rather than files.
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions