From d4f3cc324f1021bc88438c8261f36e2a5f8ee7a1 Mon Sep 17 00:00:00 2001
From: Roberto Cirillo <roberto.cirillo@isti.cnr.it>
Date: Fri, 20 Jan 2023 15:31:10 +0100
Subject: [PATCH] Update 'Jenkinsfile'

add build_options input parameter
---
 Jenkinsfile | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Jenkinsfile b/Jenkinsfile
index 030f4ef..a33822c 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -38,7 +38,10 @@ pipeline {
              description: 'The location of the local repository') 
       string(name: 'exec_label',
              defaultValue: 'CI',
-             description: 'Run on all nodes matching the label')                         
+             description: 'Run on all nodes matching the label')
+      string(name: 'build_options',
+             defaultValue: '',
+             description: 'Additional options for Maven.')                                      
     }  
     agent
     {