diff --git a/Jenkinsfile b/Jenkinsfile index 8688e750..092729cf 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -118,7 +118,7 @@ try { dir="${projectName}" [[ -d triqs_\$dir ]] && dir=triqs_\$dir || [[ -d \$dir ]] echo "160000 commit ${commit}\t\$dir" | git update-index --index-info - git commit --author='Flatiron Jenkins ' --allow-empty -m 'Autoupdate ${projectName}' -m '${env.BUILD_TAG}' + git commit --author='Flatiron Jenkins ' -m 'Autoupdate ${projectName}' -m '${env.BUILD_TAG}' git push origin ${env.BRANCH_NAME} || { git pull --rebase origin ${env.BRANCH_NAME} && git push origin ${env.BRANCH_NAME} ; } """ } catch (err) {