From 0e63817065dd414810c2151584bec5a163082cd3 Mon Sep 17 00:00:00 2001
From: Manuele Simi <manuele.simi@isti.cnr.it>
Date: Sat, 31 Aug 2019 08:54:23 -0400
Subject: [PATCH] Use pipeline-agent

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

diff --git a/Jenkinsfile b/Jenkinsfile
index 2ff4efb..8505488 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -76,8 +76,9 @@ echo "Configured dynamic stages: ${dynamicStages.inspect()}"
 
 pipeline {
    // see https://jenkins.io/doc/book/pipeline/syntax/#agent
-    agent any
-
+    agent {
+         label 'pipeline-agent'
+      }
    // see https://jenkins.io/doc/book/pipeline/syntax/#environment
    environment {
       JOB_OPTIONS = "${options}"