From e16e832f5afda62bedc9f33759db7b0f4ef76253 Mon Sep 17 00:00:00 2001
From: Manuele Simi <manuele.simi@isti.cnr.it>
Date: Sat, 16 Jan 2021 23:21:06 -0500
Subject: [PATCH] Fix syntax.

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

diff --git a/Jenkinsfile b/Jenkinsfile
index 5571300..2fe5425 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -116,7 +116,7 @@ pipeline {
  * NOTE:  'credentialsId' be manually configured in Jenkins to access all the repos
  */
 def checkout_and_exec(repo_name, actions) {
-    def repo_url = "${repo_root}/{$repo_name}"
+    def repo_url = "${repo_root}/${repo_name}"
     sh(script: "rm -r ${repo_name} || true", returnStdout: true)?.trim()
     checkout([
             $class                           : 'GitSCM',