Merge remote-tracking branch 'origin/main' into uwzhuohu_staff_page

.gitlab-ci.yml

@@ -8,7 +8,7 @@ test:
     - java GenerateSite
     # heuristic to see if any lines were removed!
     - git fetch origin main
-    - '(exit $(git diff origin/main HEAD | grep "^-[^-]" | wc -l)) || { echo "Malformed merge request: at least one line is removed in diff." && (exit 1) }'
+    - '(exit $(git diff origin/main HEAD | grep "^-[^-]" | wc -l)) || { echo "Malformed merge request: at least one line is removed in diff, or feature branch is not up-to-date with the main branch." && (exit 1) }'
 
 pages:
   tags: