From 32d66c6a7e7b7453d2a361613152e6763350581f Mon Sep 17 00:00:00 2001
From: Manuele Simi <manuele.simi@isti.cnr.it>
Date: Wed, 29 May 2019 22:25:29 -0400
Subject: [PATCH] Make the local repo path available through an environment
 variable.

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

diff --git a/Jenkinsfile b/Jenkinsfile
index 7226ea5..2cd535a 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -41,6 +41,7 @@ pipeline {
    // see https://jenkins.io/doc/book/pipeline/syntax/#environment
    environment {
       JOB_OPTIONS = "${options}"
+      MAVEN_LOCAL_REPO = "${maven_local_repo_path}"
    }
 
    // see https://jenkins.io/doc/book/pipeline/syntax/#parameters
@@ -55,8 +56,8 @@ pipeline {
         stage('clean up before starting') {
             script {
                 echo "Create a fresh local repository"
-                rm -rf "${maven_local_repo_path}"
-                mkdir -p "${maven_local_repo_path}"
+                rm -rf $MAVEN_LOCAL_REPO
+                mkdir -p $MAVEN_LOCAL_REPO
                 echo "Done with local repository"
             }
         }