Skip to content

Commit

Permalink
chore: always change pr body
Browse files Browse the repository at this point in the history
  • Loading branch information
JoeWang1127 committed Sep 16, 2024
1 parent 02eea8d commit 6b75e0c
Showing 1 changed file with 1 addition and 3 deletions.
4 changes: 1 addition & 3 deletions .github/scripts/hermetic_library_generation.sh
Original file line number Diff line number Diff line change
Expand Up @@ -101,11 +101,9 @@ git add --all -- ':!pr_description.txt' ':!hermetic_library_generation.sh'
changed_files=$(git diff --cached --name-only)
if [[ "${changed_files}" == "" ]]; then
echo "There is no generated code change."
echo "Skip committing to the pull request."
exit 0
fi

git commit -m "${message}"
git commit --allow-empty -m "${message}"
git push
# set pr body if pr_description.txt is generated.
if [[ -f "pr_description.txt" ]]; then
Expand Down

0 comments on commit 6b75e0c

Please sign in to comment.