diff --git a/jenkins_make b/jenkins_make index e041f0de6db2f0290fa4594b32fac3c1dd53a842..557a1ac541f28a55946215b763ad49fb3a9a3e9c 100755 --- a/jenkins_make +++ b/jenkins_make @@ -2,9 +2,6 @@ echo FILTERED BY $0 -# Print this script for debugging purposes, to see which filters are active -cat $0 - # Create a temporary file that contains our script. SCRIPT=`mktemp`