From 2c38138c00571e9568528a3d6f29db5b18475210 Mon Sep 17 00:00:00 2001
From: Manuele Simi <manuele.simi@isti.cnr.it>
Date: Thu, 10 Oct 2019 10:43:24 -0400
Subject: [PATCH] Change the default maven settings in the first stage and
 restore them as post-action.

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

diff --git a/Jenkinsfile b/Jenkinsfile
index 51aaac4..ec29924 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -93,6 +93,9 @@ pipeline {
                 echo "Create a fresh local repository"
                 rm -rf $MAVEN_LOCAL_REPO
                 mkdir -p $MAVEN_LOCAL_REPO
+                // default the selected maven settings
+                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"
                 '''
 
@@ -189,6 +192,22 @@ pipeline {
         }
 
     }
+
+    // post-build actions
+	post {
+        always {
+            // restore the default maven settings
+            mv "${agent_root_folder}/settings.${PIPELINE_BUILD_NUMBER}" "${agent_root_folder}/settings.xml"
+            echo 'The default maven settings have been restored'
+        }
+        success {
+            echo 'The pipeline worked!'
+        }
+        failure {
+            echo 'The pipeline has failed'
+        }
+
+    }
 }
 
 def buildComponents(args, maven_settings_file, maven_local_repo_path) {