Auto merge of #6288 - flip1995:changelog_internal, r=<try>

[WIP] Require the `changelog:` entry in the PR body to be modified

r? `@ghost` (CI PR, so expect many bors tries. Will assign later)

changelog: none

Author: bors

.github/PULL_REQUEST_TEMPLATE.md

@@ -1,8 +1,8 @@
 Thank you for making Clippy better!
 
 We're collecting our changelog from pull request descriptions.
-If your PR only updates to the latest nightly, you can leave the
-`changelog` entry as `none`. Otherwise, please write a short comment
+If your PR only includes internal changes, you can just change the
+`changelog` entry to `internal`. Otherwise, please write a short comment
 explaining your change.
 
 If your PR fixes an issue, you can add "fixes #issue_number" into this
@@ -28,5 +28,5 @@ Delete this line and everything above before opening your PR.
 
 ---
 
-*Please keep the line below*
+*Please adapt the line below (Use "internal" for internal only changes)*
 changelog: none

.github/workflows/clippy_bors.yml

@@ -40,8 +40,9 @@ jobs:
         if [[ -z "$output" ]]; then
           echo "ERROR: PR body must contain 'changelog: ...'"
           exit 1
-        elif [[ "$output" = "none" ]]; then
-          echo "WARNING: changelog is 'none'"
+        elif [[ -n $(echo "$output" | grep -i "^\s*none\.*$") ]]; then
+          echo "ERROR: changelog is 'none', use 'internal' for internal only changes"
+          exit 1
         fi
       env:
         PYTHONIOENCODING: 'utf-8'

util/fetch_prs_between.sh

@@ -15,7 +15,7 @@ for pr in $(git log --oneline --grep "Merge #" --grep "Merge pull request" --gre
   id=$(echo "$pr" | rg -o '#[0-9]{3,5}' | cut -c 2-)
   commit=$(echo "$pr" | cut -d' ' -f 1)
   message=$(git --no-pager show --pretty=medium "$commit")
-  if [[ -n $(echo "$message" | rg "^[\s]{4}changelog: [nN]one\.*$") ]]; then
+  if [[ -n $(echo "$message" | rg -i "^[\s]{4}changelog: internal\.*$") ]]; then
     continue
   fi