diff --git a/tools/build-system/launch-build-machine-jenkins.sh b/tools/build-system/launch-build-machine-jenkins.sh index 754ce8b4809e6a79e576434ad5cef33e53b083cd..2478d702f0d9789e90c98ce8914872f75685c2b4 100755 --- a/tools/build-system/launch-build-machine-jenkins.sh +++ b/tools/build-system/launch-build-machine-jenkins.sh @@ -10,7 +10,7 @@ # Last Modified: 2010-04-22 16:42:57 -0400 ##################################################### -#set -x +set -x # . `dirname $0`/setenv.sh