From 308b736541d4fdc000cf8abb1577f0d55e05c77c Mon Sep 17 00:00:00 2001 From: Redddy Date: Thu, 15 Jan 2026 23:56:14 +0900 Subject: [PATCH] Added section on using GitHub Dev for PR inspection --- src/doc/rustc-dev-guide/src/git.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/doc/rustc-dev-guide/src/git.md b/src/doc/rustc-dev-guide/src/git.md index e7e84e2ea7f5..abe72b29cb1e 100644 --- a/src/doc/rustc-dev-guide/src/git.md +++ b/src/doc/rustc-dev-guide/src/git.md @@ -495,6 +495,14 @@ command to check it out locally. See 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