Skip to content

Commit 51eeb80

Browse files
committed
add rdg push git config entry for git protocol pushers (again)
1 parent e37eb67 commit 51eeb80

File tree

1 file changed

+10
-0
lines changed

1 file changed

+10
-0
lines changed

src/external-repos.md

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,16 @@ switch to its repository checkout directory in your terminal).
8080
8181
#### Performing push
8282
83+
> NOTE:
84+
> If you use Git protocol to push to your fork of `rust-lang/rust`,
85+
> ensure that you have this entry in your Git config,
86+
> else the 2 steps that follow would prompt for a username and password:
87+
>
88+
> ```
89+
90+
> insteadOf = "https://github.com/"
91+
> ```
92+
8393
1) Run the push command to create a branch named `<branch-name>` in a `rustc` fork under the `<gh-username>` account
8494
```
8595
rustc-josh-sync push <branch-name> <gh-username>

0 commit comments

Comments
 (0)