diff options
| author | Pierre-Marie Pédrot | 2018-08-27 19:20:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-08-27 19:20:59 +0200 |
| commit | bce734bfb2a118dbb487e5b88eba524ca14d2078 (patch) | |
| tree | 8885baa7bd37813cd0ae6082b8dbd474a40adc61 /Makefile.dev | |
| parent | 85f05717483af9fb6905e4117a66d5c7bde394da (diff) | |
| parent | 99c9fb61fd702693807f0558b04e5134e08e87bb (diff) | |
Merge PR #8260: Tweak diff options in CoqIDE
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions