#echo Storing current configuration into \$WORKSPACE/$OUTPUT_FILE
OUTPUT_FILE=$WORKSPACE/$OUTPUT_FILE
echo "# Auto-generated by ${BASH_SOURCE[0]}" > $OUTPUT_FILE
#echo Storing current configuration into \$WORKSPACE/$OUTPUT_FILE
OUTPUT_FILE=$WORKSPACE/$OUTPUT_FILE
echo "# Auto-generated by ${BASH_SOURCE[0]}" > $OUTPUT_FILE