From 957f959f320311e9c0ad01a30ca9e34fdf802bc9 Mon Sep 17 00:00:00 2001 From: Remco Vermeulen Date: Thu, 14 Sep 2023 10:45:46 -0700 Subject: [PATCH] Push commits if manual was updated --- .github/workflows/prepare-release.yml | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/.github/workflows/prepare-release.yml b/.github/workflows/prepare-release.yml index c34408b9f4..f53ba60163 100644 --- a/.github/workflows/prepare-release.yml +++ b/.github/workflows/prepare-release.yml @@ -130,18 +130,11 @@ jobs: find docs -name 'user_manual.md' | xargs sed -i "s/This user manual documents release \`.*\` of/This user manual documents release \`$RELEASE_VERSION\` of/" if git diff --quiet; then - echo "update-release-pr=true" >> "$GITHUB_ENV" - else - echo "update-release-pr=false" >> "$GITHUB_ENV" + git add -u . + git commit -m "Update version" + git push fi - - name: Update feature branch for PR - if: env.update-release-pr == 'true' - run: | - find docs -name 'user_manual.md' -exec git add {} \; - git commit -m "Update user manual for release $RELEASE_VERSION." - git push - - name: Create release PR env: GITHUB_TOKEN: ${{ secrets.ACTION_DISPATCH_TOKEN }}