# HG changeset patch
# User Paul Boddie <paul@boddie.org.uk>
# Date 1529332592 -7200
# Node ID 15055ea38716195e8d009cc6b00d421a71f38369
# Parent  551e03d0550ef97d53ad021e43f004e4e51c8c3d
Conduct the configuration check quietly.

diff -r 551e03d0550e -r 15055ea38716 tools/install.sh
--- a/tools/install.sh	Mon Jun 18 16:35:58 2018 +0200
+++ b/tools/install.sh	Mon Jun 18 16:36:32 2018 +0200
@@ -50,7 +50,7 @@
 
 # Check the configuration, if possible.
 
-"$THISDIR/checkconfig.sh" "$L4DIR"
+"$THISDIR/checkconfig.sh" -q "$L4DIR"
 
 # Generate binaries if appropriate.