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) {