Skip to content

Commit

Permalink
chore: fix typo in claim-issue workflow script
Browse files Browse the repository at this point in the history
  • Loading branch information
pitmonticone committed Feb 14, 2025
1 parent 37ef129 commit f5320cc
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion .github/workflows/01-claim-issue.yml
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ jobs:
if [ "$CURRENT_STATUS_ID" != "$UNCLAIMED_TASKS_ID" ]; then
echo "Issue is not classified as 'Unclaimed'. Posting comment."
curl -X POST -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
-d '{"body": "This issue cannot be assigned to @${{ github.event.comment.user.login }} because it has not been classified as an \"Unclaimed Outstanding Task\" by the project maintainers.\n\nPlease consider discussing the issue on our [Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/416277-FLT). To understand the contribution process, please read the [CONTRIBUTING guide](https://github.com/ImperialCollegeLondon/FLT/blob/main/CONTRIBUTING.md)."}' \
-d '{"body": "This issue cannot be assigned to @${{ github.event.comment.user.login }} because it has not been classified as an \"Unclaimed\" by the project maintainers.\n\nPlease consider discussing the issue on our [Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/416277-FLT). To understand the contribution process, please read the [CONTRIBUTING guide](https://github.com/ImperialCollegeLondon/FLT/blob/main/CONTRIBUTING.md)."}' \
https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/comments
exit 1
fi
Expand Down

0 comments on commit f5320cc

Please sign in to comment.