Set GitHub credentials for pushing to clone when creating PR to remove patch

Author: jwodder

.github/workflows/tools/apply-patches

@@ -37,6 +37,7 @@ do
             tmpdir="$(mktemp -d)"
             git clone --depth 1 "$(git remote get-url origin)" "$tmpdir"
             cd "$tmpdir"
+            git config http.https://github.com/.extraheader "AUTHORIZATION: basic $(printf 'x-access-token:%s' "$GITHUB_TOKEN" | base64)"
             git checkout -b "$branch_name"
             git rm "$patchfile"
             git commit -m "Delete patch $(basename "$patchfile")"