Skip to content

Commit

Permalink
line too long?
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed Aug 2, 2024
1 parent 9166c8b commit 800110e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion .github/workflows/monthly_pr_report.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -93,4 +93,4 @@ jobs:
fi
./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}"
#./mathlib/scripts/update_PR_comment.sh "${message}" "${title}" "${PR}"

0 comments on commit 800110e

Please sign in to comment.