Set GitHub credentials for pushing to clone when creating PR to remov…

…e patch
datalad · Feb 16, 2021 · dc55451 · dc55451
1 parent 0bd62e1
commit dc55451
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.github/workflows/tools/apply-patches b/.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")"