diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-03 15:29:24 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-03 15:29:24 +0200 |
| commit | 8c99ee9b5b1212bf52fdf580525489eb8f89a682 (patch) | |
| tree | 333e46afd80ddd9ab51c452fb611d58d9a170e31 /ide/coq.lang | |
| parent | 582c1d2d152b696d0b7ec1ec8240436ae66ff326 (diff) | |
configure: fix warning printing
Diffstat (limited to 'ide/coq.lang')
0 files changed, 0 insertions, 0 deletions