diff --git a/tools/make-main-dist.sh b/tools/make-main-dist.sh
index 06df905d8d2dabf505f72c1c44a220b49b678743..581b8f500ec44ba6c04a122ad8e6647bd096eee0 100755
--- a/tools/make-main-dist.sh
+++ b/tools/make-main-dist.sh
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-set -x
+# set -x
 while getopts "G:O:bgh?" arg
 do
     case $arg in