better report

leanprover-community · Aug 2, 2024 · 0bf5e48 · 0bf5e48
1 parent e453c37
commit 0bf5e48
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/monthly_summary.sh b/monthly_summary.sh
@@ -84,14 +84,14 @@ if [ -z "${only_gh}" ]
 then
   printf $'* All PRs are accounted for!\n'
 else
-  printf $'* PRs not corresponding to a commit (merged in %s, closed in %s?)\n%s\n' "${prev_mth}" "${mth}" "${only_gh}"
+  printf $'* PRs not corresponding to a commit (CI started in %s and ended in %s?)\n%s\n' "${prev_mth}" "${mth}" "${only_gh}"
 fi
 
 if [ -z "${only_git}" ]
 then
   printf $'\n* All commits are accounted for!\n'
 else
-  printf $'\n* PRs not found by `gh` (merged in %s, closed in %s?)\n%s\n' "${mth}" "${next_mth}" "${only_git}"
+  printf $'\n* PRs not found by `gh` (CI started in %s and ended in %s?)\n%s\n' "${mth}" "${next_mth}" "${only_git}"
 fi
 
 printf -- $'---\n'