diff options
| author | Guillaume Melquiond | 2017-09-21 18:32:56 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2017-09-21 18:32:56 +0200 |
| commit | 6f039e936d5039388d969d7bf0e1763f8f5c8397 (patch) | |
| tree | 64d1cb6babae37db6a4757c84ff2dea4f275d52e /dev | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
Properly handle "coq_makefile -Q . Foo" (bug #5580).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions