Skip to content

Commit e453c37

Browse files
committed
improve docs, remove one comment
1 parent 6673741 commit e453c37

File tree

2 files changed

+4
-11
lines changed

2 files changed

+4
-11
lines changed

.github/workflows/monthly_pr_report.yaml

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,6 @@ jobs:
3333
run: |
3434
yrMth=2024-07
3535
mth="$(date -d "${yrMth}-01" '+%B')"
36-
#PR="${{ github.event.pull_request.number }}"
3736
title="### ${mth} in Mathlib summary"
3837
3938
mim="$(printf '%s\n\n%s\n' "${title}" "$(cd mathlib; ./../blog/monthly_summary.sh "${yrMth}")")"

monthly_summary.sh

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
#!/bin/bash
22

3-
# Check if required arguments are provided
3+
# Check if required argument is provided
44
if [ "$#" -ne 1 ]; then
55
printf $'Usage: %s <YYYY-MM>\n\nFor instance `%s 2024-07`\n\n' "${0}" "${0}"
66
exit 1
@@ -16,15 +16,12 @@ repository='leanprover-community/mathlib4'
1616
startDate="${1}"
1717
endDate="${2}"
1818

19-
# find how many commits to master there have been in the last month
19+
# find how many commits to master there have been in the given range -- note that there is a limit to how many commits `gh` returns
2020
commits_in_range="$(git log --since="${startDate}" --until="${endDate}" --pretty=oneline | wc -l)"
2121

22-
# Retrieve merged PRs from the given range
22+
# Retrieve merged (i.e. closed, due to bors) PRs from the given range
2323
prs=$(gh pr list --repo "$repository" --state closed --base master --search "closed:${startDate}..${endDate}" --json number,labels,title,author --limit "$((commits_in_range * 2))")
2424

25-
## Print PR numbers, their labels and their title
26-
#echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "PR #\(.number) - Labels: \((.labels | map(.name) | join(", ")) // "No labels") - Title: \(.title)"'
27-
2825
# Store to file `found_by_gh.txt` the PR numbers, as found by `gh`
2926
echo "$prs" | jq -r '.[] | select(.title | startswith("[Merged by Bors]")) | "(#\(.number))"' | sort >> found_by_gh.txt
3027

@@ -35,7 +32,7 @@ git log --pretty=oneline --since="${startDate}" --until="${endDate}" |
3532
echo "$prs"
3633
}
3734

38-
# the current year and month
35+
# the year and month being processed
3936
yr_mth="${1}" #"$(date +%Y-%m)"
4037
yr_mth_day=${yr_mth}-01
4138

@@ -52,9 +49,6 @@ printf $'\n\nBetween %s and %s there were\n' "${yr_mth_day}" "${end_date/%T*}"
5249

5350
printf $'* %s commits to `master` and\n' "${commits_in_range}"
5451

55-
#echo "First run: ${start_date} ${yr_mth}-15T23:59:59"
56-
#echo "Second run: ${yr_mth}-16T00:00:00 ${end_date}"
57-
5852
(
5953
findInRange "${start_date}" "${yr_mth}-15T23:59:59" | sed -z 's=]\n*$=,\n='
6054
findInRange "${yr_mth}-16T00:00:00" "${end_date}" | sed -z 's=^\[=='

0 commit comments

Comments
 (0)