From 2f4f1a46d888515c093641d49b24df0557810cd0 Mon Sep 17 00:00:00 2001
From: Manuele Simi <manuele.simi@isti.cnr.it>
Date: Wed, 25 Sep 2019 09:47:49 -0400
Subject: [PATCH] Forgot to quote maven-parent.

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

diff --git a/Jenkinsfile b/Jenkinsfile
index 1b9d98c..68caf57 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -98,7 +98,7 @@ pipeline {
         stage('build maven-parent') {
           steps {
                 withMaven(jdk: "${maven_jdk}", mavenLocalRepo: "${maven_local_repo_path}", mavenSettingsFilePath: "${maven_settings_file}") {
-                    build maven-parent
+                    build 'maven-parent'
                 }
                 echo "Done with maven-parent"
           }