From ebd85184ee28c088bd84a02183295ce9268c91d6 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Mon, 22 Jul 2024 18:24:48 +0200
Subject: [PATCH] [ci] Guarding update date headers
---
Makefile | 1 +
update_headers.sh | 15 ++++++++++++---
2 files changed, 13 insertions(+), 3 deletions(-)
diff --git a/Makefile b/Makefile
index 8002cd9..12dc6ee 100644
--- a/Makefile
+++ b/Makefile
@@ -48,6 +48,7 @@ DESCRIPTION="$(shell sed -n -e "p;n;:next;/^##/Q;p;n;b next" CHANGES.md | perl -
release:
@echo "Proceed to release CAISAR with release version $(TAG)? (y/n)?"
@read yesno; test "$$yesno" = y
+ @bash update_headers.sh
@echo -n $(DESCRIPTION)
@echo "Is the CHANGES.md correct for $(TAG) (y/n)?"
@read yesno; test "$$yesno" = y
diff --git a/update_headers.sh b/update_headers.sh
index 7406ccd..54603c9 100644
--- a/update_headers.sh
+++ b/update_headers.sh
@@ -1,5 +1,14 @@
#!/usr/bin/env bash
-set -xe
+# set -xe
NEW_DATE=$(date "+%Y")
-OLD_DATE=$(date -d '1 year ago' "+%Y")
-find . \( -type d -name .git -prune \) \( -type d -name ._build -prune \) -o -type f -print0 | xargs -0 sed -i 's/(C) '${OLD_DATE}'/(C) '${NEW_DATE}'/g'
\ No newline at end of file
+OLD_DATE=$(sed "5q;d" src/main.ml | awk '{print $4}')
+
+if [ "$OLD_DATE" != "$NEW_DATE" ]; then
+ echo "Replacing $OLD_DATE by $NEW_DATE in headers."
+ find . \( -type d -name .git -prune \) \( -type d -name ._build -prune \) -o -type f -print0 | xargs -0 sed -i 's/(C) '${OLD_DATE}'/(C) '${NEW_DATE}'/g'
+ echo "Done."
+ exit 0
+else
+ echo "Year $OLD_DATE in header src/main.ml is current date, no need to update the headers."
+ exit 0
+fi
--
GitLab