File tree Expand file tree Collapse file tree 1 file changed +6
-3
lines changed Expand file tree Collapse file tree 1 file changed +6
-3
lines changed Original file line number Diff line number Diff line change 3
3
: << 'BASH_DOC_MODULE '
4
4
5
5
Running `monthly_summary.sh 2024-07` produces an md-formatted summary of all the PRs that were
6
- merged into mathlib master in the month 2024-07
6
+ merged into mathlib master in the month 2024-07.
7
+ A "raw" format can be obtain running `monthly_summary.sh 2024-07 raw`.
8
+
9
+ There is a slight discrepancy
7
10
8
11
BASH_DOC_MODULE
9
12
114
117
printf -- $' ---\n '
115
118
116
119
rm -rf found_by_gh.txt found_by_git.txt
117
- } | if [ " ${raw} " == " raw" ]; then cat; else # extra .md formatting
120
+ } | { if [ " ${raw} " == " raw" ]; then cat; else # extra .md formatting
118
121
sed '
119
122
/ [0-9]* PRs$/{
120
123
s=^=</details><details><summary>\n=
@@ -126,4 +129,4 @@ rm -rf found_by_gh.txt found_by_git.txt
126
129
s=\n---\nReports\n\n=\n</details>\n\n---\n\n<details><summary>Reports</summary>\n\n=
127
130
s=\n---[\n]*$=\n\n</details>\n&=
128
131
'
129
- fi
132
+ fi }
You can’t perform that action at this time.
0 commit comments