From 146303c77f23336c0894c71f7977653d7cf0efd4 Mon Sep 17 00:00:00 2001
From: Manuele Simi <manuele.simi@isti.cnr.it>
Date: Mon, 21 Oct 2019 21:28:21 -0400
Subject: [PATCH] Output ${AGENT_ROOT_FOLDER}/build_commits.txt.

---
 Jenkinsfile | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Jenkinsfile b/Jenkinsfile
index 4495a40..21ff2a6 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -120,6 +120,7 @@ pipeline {
                 mv "${AGENT_ROOT_FOLDER}/settings.xml" "${AGENT_ROOT_FOLDER}/settings.${PIPELINE_BUILD_NUMBER}"
                 cp "${AGENT_ROOT_FOLDER}/${MAVEN_SETTINGS_FILE}" "${AGENT_ROOT_FOLDER}/settings.xml"
                 echo "Done with local repository and settings"
+                cat "Build #${PIPELINE_BUILD_NUMBER}" > ${AGENT_ROOT_FOLDER}/build_commits.txt
                 '''
             }
         }
@@ -242,6 +243,7 @@ pipeline {
              script {
                   sh '''
                   mv "${AGENT_ROOT_FOLDER}/settings.${PIPELINE_BUILD_NUMBER}" "${AGENT_ROOT_FOLDER}/settings.xml"
+                  mv  ${AGENT_ROOT_FOLDER}/build_commits.txt  ${AGENT_ROOT_FOLDER}/build_commits.${PIPELINE_BUILD_NUMBER}
                   '''
              }
              echo 'The default maven settings have been restored'