diff options
| author | Emilio Jesus Gallego Arias | 2019-05-25 20:52:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-25 20:52:30 +0200 |
| commit | 51dc650f8b47a7381c19376793871817f2ef9578 (patch) | |
| tree | 95baa9812c7aade24e4197b52d1c0aa3252d229f /library | |
| parent | 9241a6e25ff132a27762963b06ae1095c783c25f (diff) | |
| parent | f6811213b24b5646404d3f3ad48a4ec79eb12dab (diff) | |
Merge PR #10244: Coqc: Treat unknown arguments starting with dash as unknown options rather than files
Reviewed-by: ejgallego
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions