From e5d884cbdc6fe51317c72754fea89595a2fd3b8f Mon Sep 17 00:00:00 2001 From: dany Date: Tue, 20 Sep 2022 14:54:59 +0200 Subject: [PATCH] Update 'Jenkinsfile' --- Jenkinsfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Jenkinsfile b/Jenkinsfile index 3ce4fed..08b26ba 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -6,7 +6,7 @@ remote.identityFile = '/var/jenkins_home/.ssh/id_rsa' remote.allowAnyHosts = true remote.agent = false remote.logLevel = 'INFO' -def build_appimage() +def copylib() { sh ''' set -e