From 1baccd90d4badb994e0007e5e06a7449219da49d Mon Sep 17 00:00:00 2001
From: andreacavalli <andrea@warp.ovh>
Date: Fri, 9 Oct 2020 10:21:03 +0200
Subject: [PATCH] Update 'Jenkinsfile'

---
 Jenkinsfile | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Jenkinsfile b/Jenkinsfile
index fa9c307..8fc3ee1 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -15,6 +15,9 @@ pipeline {
 		booleanParam(name: "RELEASE",
 			description: "Build a release from current commit.",
 			defaultValue: false)
+		booleanParam(name: "DEBUGINFO",
+			description: "Build debug binary from current commit.",
+			defaultValue: false)
 	}
 	stages {
 		stage("Setup workspace") {
@@ -57,7 +60,7 @@ pipeline {
 				}
 			}
 			steps {
-				sh "./jenkins/scripts/cross_compile.sh"
+				sh "DEBUGINFO=${params.DEBUGINFO} ./jenkins/scripts/cross_compile.sh"
 			}
 		}