user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #2728 from reddevilmidzy/tip

Browse source 
Added section on using GitHub Dev for PR inspection
This commit is contained in:
Boxy 2026-01-17 16:59:49 +00:00 • committed by GitHub
commit 2f393eb725
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/doc/rustc-dev-guide/src/git.md
View file

@ -495,6 +495,14 @@ command to check it out locally. See <https://cli.github.com/> for more info.
![`gh` suggestion](./img/github-cli.png)
### Using GitHub dev
As an alternative to the GitHub web UI, GitHub Dev provides a web-based editor for browsing
repository and PRs. It can be opened by replacing `github.com` with `github.dev` in the URL
or by pressing `.` on a GitHub page.
See [the docs for github.dev editor](https://docs.github.com/en/codespaces/the-githubdev-web-based-editor)
for more details.
### Moving large sections of code
Git and Github's default diff view for large moves *within* a file is quite poor; it will show each