From 804f285b82750c0c9ed477382a9a81f3329229fc Mon Sep 17 00:00:00 2001
From: Manuele Simi <manuele.simi@isti.cnr.it>
Date: Wed, 29 May 2019 21:56:05 -0400
Subject: [PATCH] Build only on agents labeled as 'pipeline-agent'.

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

diff --git a/Jenkinsfile b/Jenkinsfile
index a05f07f..8d5c345 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -32,7 +32,7 @@ echo "Use local repo at ${maven_local_repo_path}"
 
 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 {