[jenkins] Make sure to update packaging repo in Jenkins CI

Jenkinsfile

@@ -62,40 +62,20 @@ for (int i = 0; i < dockerPlatforms.size(); i++) {
 def error = null
 try {
   parallel platforms
-  if (false/*keepInstall*/) { node('linux && docker && triqs') {
+  if (keepInstall) { node('linux && docker && triqs') {
     /* Publish results */
     stage("publish") { timeout(time: 5, unit: 'MINUTES') {
       def commit = sh(returnStdout: true, script: "git rev-parse HEAD").trim()
       def release = env.BRANCH_NAME == "master" || env.BRANCH_NAME == "unstable" || sh(returnStdout: true, script: "git describe --exact-match HEAD || true").trim()
       def workDir = pwd(tmp:true)
       lock('triqs_publish') {
-      /* Update documention on gh-pages branch */
-      dir("$workDir/gh-pages") {
-        def subdir = "${projectName}/${env.BRANCH_NAME}"
-        git(url: "ssh://[email protected]/TRIQS/TRIQS.github.io.git", branch: "master", credentialsId: "ssh", changelog: false)
-        sh "rm -rf ${subdir}"
-        docker.image("flatironinstitute/${dockerName}:${env.BRANCH_NAME}-${documentationPlatform}").inside() {
-          sh """#!/bin/bash -ex
-            base=\$INSTALL/share/doc
-            dir="${projectName}"
-            [[ -d \$base/triqs_\$dir ]] && dir=triqs_\$dir || [[ -d \$base/\$dir ]]
-            cp -rp \$base/\$dir ${subdir}
-          """
-        }
-        sh "git add -A ${subdir}"
-        sh """
-          git commit --author='Flatiron Jenkins <[email protected]>' --allow-empty -m 'Generated documentation for ${subdir}' -m '${env.BUILD_TAG} ${commit}'
-        """
-        // note: credentials used above don't work (need JENKINS-28335)
-        sh "git push origin master"
-      }
       /* Update packaging repo submodule */
       if (release) { dir("$workDir/packaging") { try {
         git(url: "ssh://[email protected]/TRIQS/packaging.git", branch: env.BRANCH_NAME, credentialsId: "ssh", changelog: false)
         // note: credentials used above don't work (need JENKINS-28335)
         sh """#!/bin/bash -ex
           dir="${projectName}"
-          [[ -d triqs_\$dir ]] && dir=triqs_\$dir || [[ -d \$dir ]]
+          [[ -d \$dir ]] && dir=\$dir || [[ -d \$dir ]]
           echo "160000 commit ${commit}\t\$dir" | git update-index --index-info
           git commit --author='Flatiron Jenkins <[email protected]>' -m 'Autoupdate ${projectName}' -m '${env.BUILD_TAG}'
           git push origin ${env.BRANCH_NAME}