From ce4d9baf486eba8e3d7fbf5fd153664916be9f68 Mon Sep 17 00:00:00 2001
From: Roberto Cirillo <roberto.cirillo@isti.cnr.it>
Date: Tue, 7 Feb 2023 16:32:25 +0100
Subject: [PATCH] change git fetch command

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

diff --git a/Jenkinsfile b/Jenkinsfile
index dccf3f9..9f6fb21 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -152,7 +152,7 @@ def push(repo_url, repo_name, tag, gCube_release_version, commit) {
             def repository = repo_url.replaceFirst(".+://", "https://${GIT_USERNAME}:${GIT_PASSWORD}@")
             sh("""
             git remote set-url origin $repository
-            git fetch
+            git fetch --all
             mvn clean generate-resources
             """)
         }