Jenkinsfile : regenerated with zproject support for DO_DIST_DOCS option

Jenkinsfile

@@ -34,6 +34,10 @@ pipeline {
             defaultValue: true,
             description: 'Attempt a build with docs in this run? (Note: corresponding tools are required in the build environment)',
             name: 'DO_BUILD_DOCS')
+        booleanParam (
+            defaultValue: false,
+            description: 'Publish as an archive a "dist" tarball from a build with docs in this run? (Note: corresponding tools are required in the build environment; enabling this enforces DO_BUILD_DOCS too)',
+            name: 'DO_DIST_DOCS')
         booleanParam (
             defaultValue: true,
             description: 'Attempt "make check" in this run?',
@@ -132,12 +136,19 @@ pipeline {
                     }
                 }
                 stage ('build with DOCS') {
-                    when { expression { return ( params.DO_BUILD_DOCS ) } }
+                    when { expression { return ( params.DO_BUILD_DOCS || params.DO_DIST_DOCS ) } }
                     steps {
                       dir("tmp/build-DOCS") {
                         deleteDir()
                         unstash 'prepped'
                         sh 'CCACHE_BASEDIR="`pwd`" ; export CCACHE_BASEDIR; ./configure --enable-drafts=yes --with-docs=yes'
+                        script {
+                            if ( params.DO_DIST_DOCS ) {
+                                sh 'CCACHE_BASEDIR="`pwd`" ; export CCACHE_BASEDIR; make dist-gzip || exit ; DISTFILE="`ls -1tc *.tar.gz | head -1`" && [ -n "$DISTFILE" ] && [ -s "$DISTFILE" ] || exit ; mv -f "$DISTFILE" __dist.tar.gz'
+                                archiveArtifacts artifacts: '__dist.tar.gz'
+                                sh "rm -f __dist.tar.gz"
+                            }
+                        }
                         sh 'CCACHE_BASEDIR="`pwd`" ; export CCACHE_BASEDIR; make -k -j4 || make'
                         sh 'echo "Are GitIgnores good after make with docs? (should have no output below)"; git status -s || if [ "${params.REQUIRE_GOOD_GITIGNORE}" = false ]; then echo "WARNING GitIgnore tests found newly changed or untracked files" >&2 ; exit 0 ; else echo "FAILED GitIgnore tests" >&2 ; exit 1; fi'
                         stash (name: 'built-docs', includes: '**/*', excludes: '**/cppcheck.xml')
@@ -332,10 +343,13 @@ pipeline {
                         if ( env.BRANCH_NAME =~ myDEPLOY_BRANCH_PATTERN ) {
                             def GIT_URL = sh(returnStdout: true, script: """git remote -v | egrep '^origin' | awk '{print \$2}' | head -1""").trim()
                             def GIT_COMMIT = sh(returnStdout: true, script: 'git rev-parse --verify HEAD').trim()
+                            def DIST_ARCHIVE = ""
+                            if ( params.DO_DIST_DOCS ) { DIST_ARCHIVE = env.BUILD_URL + "artifact/__dist.tar.gz" }
                             build job: "${myDEPLOY_JOB_NAME}", parameters: [
                                 string(name: 'DEPLOY_GIT_URL', value: "${GIT_URL}"),
                                 string(name: 'DEPLOY_GIT_BRANCH', value: env.BRANCH_NAME),
-                                string(name: 'DEPLOY_GIT_COMMIT', value: "${GIT_COMMIT}")
+                                string(name: 'DEPLOY_GIT_COMMIT', value: "${GIT_COMMIT}"),
+                                string(name: 'DEPLOY_DIST_ARCHIVE', value: "${DIST_ARCHIVE}")
                                 ], quietPeriod: 0, wait: myDEPLOY_REPORT_RESULT, propagate: myDEPLOY_REPORT_RESULT
                         } else {
                             echo "Not deploying because branch '${env.BRANCH_NAME}' did not match filter '${myDEPLOY_BRANCH_PATTERN}'"