Skip to content

Commit

Permalink
many printf
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed May 18, 2024
1 parent bd49498 commit ecb1d75
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion scripts/mathlib_stats.sh
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,12 @@ declSummary="$(paste -d' ' <(echo "${newDecls}") <(echo "${oldDecls}") |
)"

## final report
printf -- '---\n\n## Weekly stats (%s %(%Y-%m-%d)T)\n\n%s, %s total(insertions-deletions)\n\n---\n\n%s\n\n commits: old %s, current %s.\n\nDeclarations:\n%s\n\nTake also a look at the [`Mathlib` stats page](%s).\n' "${date}" -1 "${gdiff}" "${net}" "${percent}" "${oldCommitURL}" "${currentCommitURL}" "${declSummary}" "${statsURL}"
printf -- '---\n\n## Weekly stats (%s %(%Y-%m-%d)T)\n\n' "${date}" -1

printf -- '%s, %s total(insertions-deletions)\n\n---\n\n%s' "${gdiff}" "${net}" "${percent}"

printf -- '\n\n commits: old %s, current %s.\n\n' "${oldCommitURL}" "${currentCommitURL}"

printf -- 'Declarations:\n%s\n\nTake also a look at the [`Mathlib` stats page](%s).\n' "${declSummary}" "${statsURL}"

git checkout -q "${currentCommit}" > /dev/null

0 comments on commit ecb1d75

Please sign in to comment.