From da8862ffb4351eb60d459eb13c2caf07f0a08e73 Mon Sep 17 00:00:00 2001
From: Sebastiaan Speck <12570668+sebastiaanspeck@users.noreply.github.com>
Date: Tue, 10 Sep 2024 19:21:59 +0200
Subject: [PATCH] CI: check if the page title is up-to-date (#13654)

---
 scripts/check-pr.sh | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/scripts/check-pr.sh b/scripts/check-pr.sh
index 70efc012e..a9c82c1ce 100755
--- a/scripts/check-pr.sh
+++ b/scripts/check-pr.sh
@@ -121,6 +121,16 @@ function check_more_info_link() {
   fi
 }
 
+function check_page_title() {
+  local page=$1
+
+  grep "$page" "page-titles.txt" > /dev/null
+
+  if [ $? -eq 0 ]; then
+      printf "\x2d $MSG_PAGE_TITLE" "$page"
+  fi
+}
+
 # Look at git diff and check for copied/duplicated pages.
 function check_diff {
   local git_diff
@@ -137,6 +147,7 @@ function check_diff {
   fi
 
   python3 scripts/set-more-info-link.py -Sn > more-info-links.txt
+  python3 scripts/set-page-title.py -Sn > page-titles.txt
 
   while read line; do
     readarray -td$'\t' entry < <(echo -n "$line")
@@ -159,11 +170,13 @@ function check_diff {
         check_missing_english_page "$file1"
         check_outdated_page "$file1"
         check_more_info_link "$file1"
+        check_page_title "$file1"
         ;;
       M) # file1 was modified
         check_missing_english_page "$file1"
         check_outdated_page "$file1"
         check_more_info_link "$file1"
+        check_page_title "$file1"
         ;;
     esac
   done <<< "$git_diff"
@@ -198,6 +211,7 @@ MSG_NOT_DIR='The file `%s` does not look like a directory.\n'
 MSG_NOT_FILE='The file `%s` does not look like a regular file.\n'
 MSG_NOT_MD='The file `%s` does not have a `.md` extension.\n'
 MSG_MORE_INFO='The page `%s` has an outdated more info link.\n'
+MSG_PAGE_TITLE='The page `%s` has an outdated page title.\n'
 
 PLATFORMS=$(ls pages/)