Push commits if manual was updated

github · Sep 14, 2023 · 957f959 · 957f959
1 parent f93888a
commit 957f959
Showing 1 changed file with 3 additions and 10 deletions.
diff --git 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 }}