From e42798135c2625b9c8456f7a74a3d8dfb4c52a83 Mon Sep 17 00:00:00 2001
From: Ralph Bean <rbean@redhat.com>
Date: Aug 06 2018 14:33:29 +0000
Subject: Fix doc publication.


We can use GIT_BRANCH now that @jmolet updated our jenkins plugins.

---

diff --git a/Jenkinsfile b/Jenkinsfile
index 91d1802..b123143 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -50,9 +50,7 @@ node('fedora') {
         sh 'make -C docs html'
         archiveArtifacts artifacts: 'docs/_build/html/**'
     }
-    /* Can't use GIT_BRANCH because of this issue https://issues.jenkins-ci.org/browse/JENKINS-35230 */
-    def git_branch = sh(returnStdout: true, script: 'git rev-parse --abbrev-ref HEAD').trim()
-    if (git_branch == 'master') {
+    if (scmVars.GIT_BRANCH == 'origin/master') {
         stage('Publish Docs') {
             sshagent (credentials: ['pagure-waiverdb-deploy-key']) {
                 sh '''