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" } }