diff options
| author | Maxime Dénès | 2017-10-03 12:11:50 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-03 12:11:50 +0200 |
| commit | 23ea4e3110fc4ec2da7d06ee009a1d30418e2493 (patch) | |
| tree | bcb0fb3dbf1d4e1386015cf8b6060905bdf56c2d /dev | |
| parent | c2c4a0566d5ec93f48de29dfdad2e4d3c1cec32d (diff) | |
| parent | 6f039e936d5039388d969d7bf0e1763f8f5c8397 (diff) | |
Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions