Merge pull request #3086 from rubenk/reduce-configure-noise
authorPavel Rochnyak <pavel2000@ngs.ru>
Tue, 19 Feb 2019 08:14:30 +0000 (15:14 +0700)
committerGitHub <noreply@github.com>
Tue, 19 Feb 2019 08:14:30 +0000 (15:14 +0700)
Reduce the amount of output from ./configure


Trivial merge