From d6078abdbfef8f8d4aab703109212152137d2e37 Mon Sep 17 00:00:00 2001 From: Ruben Abad Date: Tue, 4 Jun 2024 12:12:57 +0200 Subject: [PATCH] reverting previous change: repo checkout is neccessary to have access to makefile --- Jenkinsfile | 1 - 1 file changed, 1 deletion(-) diff --git a/Jenkinsfile b/Jenkinsfile index 3cae36aa6..b3fd05fef 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -208,7 +208,6 @@ pipeline stage('ubuntu smoke tests') { agent { label "gpu_20_04" } - options{skipDefaultCheckout()} steps { unstash name: 'ubuntu_eggs'