diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-29 13:44:11 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-29 13:44:11 +0100 |
| commit | 6032ce4f548e88cf341b28dc70d48b9edf6e4f09 (patch) | |
| tree | 94b8a23a219ede20d5dda67196ae6b1ed9a7d3b0 /configure.ml | |
| parent | 3624d943513ff1d79fdadf5b231ffcd3786b16c8 (diff) | |
| parent | 9f1d36749529eb66d834d4b417cbc1d8e7cac325 (diff) | |
Merge PR #6492: Remove query-in-IDE warning.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions