From 459450afad21c551c6d2fa2884219e5f62d47c4b Mon Sep 17 00:00:00 2001
From: Roberto Cirillo <roberto.cirillo@isti.cnr.it>
Date: Fri, 4 Mar 2022 11:30:36 +0100
Subject: [PATCH] assign to maven_parent_file maven_settings_file value

---
 Jenkinsfile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Jenkinsfile b/Jenkinsfile
index b411aa2..a95eed5 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -46,6 +46,7 @@ if (params.Type == 'RELEASE') {
     maven_activation_property="-Djenkins-releases -DRelease";
  //   maven_parent_file = "jenkins-releases-dry-run-settings.xml"
 }
+maven_parent_file=maven_settings_file;
 
 echo "Use settings file at ${maven_settings_file} with the following activation property: ${maven_activation_property}"
 echo "Use local repo at ${maven_local_repo_path}"