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

…e patch
datalad · Feb 16, 2021 · cf14a7b · cf14a7b
1 parent 0bd62e1
commit cf14a7b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/tools/apply-patches b/.github/workflows/tools/apply-patches
@@ -35,7 +35,7 @@ do
             echo "[INFO] Branch $branch_name already exists; assuming PR already exists"
         else
             tmpdir="$(mktemp -d)"
-            git clone --depth 1 "$(git remote get-url origin)" "$tmpdir"
+            git clone --depth 1 "$(git remote get-url origin | sed "s,https://,https://x-access-token:$GITHUB_TOKEN@,")" "$tmpdir"
             cd "$tmpdir"
             git checkout -b "$branch_name"
             git rm "$patchfile"