diff options
| author | Maxime Dénès | 2017-09-04 16:11:14 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-05 17:12:00 +0200 |
| commit | df7f4445e73d7b47a3964fa477c533e6084eaa6f (patch) | |
| tree | 1737956abfb56d703023418c4004e244719f3611 /dev/include | |
| parent | 802af9272442815012532818cffb6908ad5707e1 (diff) | |
Remove -debug option from Windows build script.
It is no longer accepted by Coq's ./configure.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions