Skip to content

Commit

Permalink
update script
Browse files Browse the repository at this point in the history
  • Loading branch information
YaelDillies committed Jul 1, 2024
1 parent 9e86099 commit ade6c80
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions monthly-blog.sh → month-in-mathlib.sh
100755 → 100644
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
#!/bin/bash

usage () {
echo "Usage: monthly-blog.sh YYYY M path/to/mathlib"
echo "Usage: month-in-mathlib.sh YYYY M path/to/mathlib4"
echo ""
echo "Where YYYY is a 4-digit year, and M is the number of the month."
echo "Example: monthly-blog.sh 2021 8 ~/mathlib"
echo "where YYYY is a 4-digit year, and M is the number of the month."
echo "Example: month-in-mathlib.sh 2021 8 ~/mathlib4"
echo "It is important that M is a natural number between 1 and 12."
echo "The formats '02' and '2' are both allowed."
echo ""
echo "Important: make sure that the mathlib clone is clean,"
echo "Important: make sure that the mathlib4 clone is clean,"
echo "and points to an up-to-date copy of master."
exit 1
}
Expand Down Expand Up @@ -37,7 +37,7 @@ echo "has_math: true"
echo "link: ''"
echo "slug: month-in-mathlib-${month_lc}-$year"
echo "tags: ''"
echo "title: This month in mathlib (${month_uc} $year)"
echo "title: This month in Mathlib (${month_uc} $year)"
echo "type: text"
echo "---"

Expand Down

0 comments on commit ade6c80

Please sign in to comment.