Skip to content

Commit

Permalink
chore: fix typo from #3148 in pr-release bot (#3154)
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Jan 10, 2024
1 parent e924ef2 commit 4e16eb0
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion .github/workflows/pr-release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,7 @@ jobs:
-X POST \
-H "Authorization: token ${{ secrets.MATHLIB4_BOT }}" \
-H "Accept: application/vnd.github.v3+json" \
-d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body": "$intro + "\n" + $val}')" \
-d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body": $intro + "\n" + $val}')" \
"https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
else
# Append new result to the existing comment
Expand Down

0 comments on commit 4e16eb0

Please sign in to comment.