Add a banner to the package promotion logging.

no issue #

Arvados-DCO-1.1-Signed-off-by: Peter Amstutz <peter.amstutz@curii.com>

diff --git a/jenkins/testing_to_stable_publish_packages.sh b/jenkins/testing_to_stable_publish_packages.sh
index 835a269006226065c8e744feec02252b79631375..ecf918e5b18dd2eb431713dfdbd1204a24891307 100755 (executable)
--- a/jenkins/testing_to_stable_publish_packages.sh
+++ b/jenkins/testing_to_stable_publish_packages.sh
@@ -46,6 +46,9 @@ CENTOS_PACKAGES=$(echo ${packages} | sed 's/\([a-z-]*\):[[:blank:]]*\([0-9.-]*\)
 DEBIAN_PACKAGES=$(echo ${packages} | sed 's/\([a-z-]*\):[[:blank:]]*\([0-9.-]*\)/\1 (= \2)/g;')
 
 for DISTNAME in ${DIST_LIST}; do
+    echo
+    echo "### Publishing packages for ${DISTNAME} ###"
+    echo
     if ( echo ${DISTNAME} |grep -q -E '(centos|rocky)' ); then
        case ${DISTNAME} in
            'centos7')