From ade6c8007c034a0409a72d1da8fcba9ef5dadc40 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 1 Jul 2024 15:39:08 +0200 Subject: [PATCH] update script --- monthly-blog.sh => month-in-mathlib.sh | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) rename monthly-blog.sh => month-in-mathlib.sh (81%) mode change 100755 => 100644 diff --git a/monthly-blog.sh b/month-in-mathlib.sh old mode 100755 new mode 100644 similarity index 81% rename from monthly-blog.sh rename to month-in-mathlib.sh index 81266899..08ce5002 --- a/monthly-blog.sh +++ b/month-in-mathlib.sh @@ -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 } @@ -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 "---"