update GitHub.dev to VSCode.dev/GitHub

source/ch-coding.ptx

@@ -4,7 +4,7 @@
   <section xml:id="sec-codespaces">
     <title>Codespaces</title>
     <p>
-While the quick <c>GitHub.dev</c> interface we used
+While the quick <c>VSCode.dev/GitHub</c> interface we used
 to get started in <xref ref="ch-first-repo"/> is great
 for quick uploads or edits, many projects require the ability
 to run applications and execute code as you would on
@@ -34,29 +34,29 @@ the green <q>Create codespace on [branchname]</q> button.
     </note>
     <p>
 After the Codespace boots up, you'll have an interface similar
-to the <c>GitHub.dev</c> environment you learned about in
+to the <c>VSCode.dev/GitHub</c> environment you learned about in
 <xref ref="sec-using-github-dev"/>.
     </p>
     <note xml:id="dev-codespace-contrast">
       <p>
 Here are a few key differences between
-<c>GitHub.dev</c> and Codespaces.
+<c>VSCode.dev/GitHub</c> and Codespaces.
         <ol>
           <li>
             <p>
-A <c>GitHub.dev</c> URL looks like <c>github.dev/username/reponame</c>,
+A <c>VSCode.dev/GitHub</c> URL looks like <c>VSCode.dev/GitHub/username/reponame</c>,
 while a Codespace URL looks like
 <c>random-word-123randomcharacters789.github.dev</c>.
             </p>
           </li>
           <li>
             <p>
-<c>GitHub.dev</c> is quicker to load than a Codespace.
+<c>VSCode.dev/GitHub</c> is quicker to load than a Codespace.
             </p>
           </li>
           <li>
             <p>
-<c>GitHub.dev</c> has a much more limited selection of VS Code
+<c>VSCode.dev/GitHub</c> has a much more limited selection of VS Code
 extensions to use.
             </p>
           </li>
@@ -69,7 +69,7 @@ You can only install applications and execute code on a Codespace.
       </p>
     </note>
     <p>
-One similarity between <c>GitHub.dev</c> and Codespaces
+One similarity between <c>VSCode.dev/GitHub</c> and Codespaces
 (besides the obviously similar VS Code user interfaces),
 is that your work is still private to you and can only be
 shared with the public (and retained in the long term) by
@@ -310,7 +310,7 @@ your Codespace will be retained before it is deleted
     <p>
 Putting it all together, we have seen three ways to access files on your repo.
 Going from the least easy to edit to the most editable we have: <c>GitHub.com</c>,
-<c>GitHub.dev</c>, <c>random-codespace-string.github.dev</c>.
+<c>VSCode.dev/GitHub</c>, <c>random-codespace-string.github.dev</c>.
 Here is what these environments look like.
     </p>
     <figure xml:id="fig-faces-of-github">

source/ch-collaboration.ptx

@@ -28,7 +28,7 @@ need their own GitHub account, and must accept the invitation to
 collaborate before gaining access.
     </p>
     <p>
-Once they have access, a collaborator can either use <c>GitHub.dev</c>
+Once they have access, a collaborator can either use <c>VSCode.dev/GitHub</c>
 (<xref ref="opening-github-dev"/>) or create their own
 Codespace (<xref ref="def-codespaces"/>).
     </p>
@@ -53,7 +53,7 @@ repository is to <em>never directly commit to the <c>main</c> branch</em>,
 even if you're the owner.
       </p>
       <p>
-To commit to an alternative branch in <c>GitHub.dev</c> or Codespaces, select
+To commit to an alternative branch in <c>VSCode.dev/GitHub</c> or Codespaces, select
 <c>main</c> in the bottom toolbar, then type the name of your new branch,
 and select <q>Create new branch</q>. It's a good idea to name your
 branch in the form <c>UserName/short-description-of-topic</c>,
@@ -90,7 +90,7 @@ or <term>ready to review</term>.
     </definition>
     <note>
       <p>
-Depending on whether the collaborator is using <c>GitHub.dev</c> or
+Depending on whether the collaborator is using <c>VSCode.dev/GitHub</c> or
 Codespaces, they may be prompted to create a pull request when first
 pushing/syncing changes. If not, a pull request can be created by
 navigating to the repository page on <c>GitHub.com</c>.
@@ -176,7 +176,7 @@ is a quick-enough fix nonetheless.
     <warning>
       <p>
         This fix must be done in a Codespace,
-        not GitHub.dev.
+        not VSCode.dev/GitHub.
       </p>
     </warning>
     <note>

source/ch-first-repo.ptx

@@ -126,7 +126,7 @@ down the line.
         </p>
     </section>
     <section xml:id="sec-using-github-dev">
-        <title>Using <c>GitHub.dev</c></title>
+        <title>Using <c>VSCode.dev/GitHub</c></title>
         <p>
 Using the <c>GitHub.com</c> interface to author or edit just one file
 can be useful (I do this all the time to make quick typo fixes on
@@ -137,7 +137,7 @@ that you need to include in your work as well.
         </p>
         <p>
 One way to quickly be able to manage several files at once is
-to use the <url href="https://github.dev">GitHub.dev</url> service
+to use the <url href="https://VSCode.dev/GitHub">VSCode.dev/GitHub</url> service
 offered by GitHub. Try clicking that link - you should have a
 fully-functional VS Code text editor right inside your web browser.
         </p>
@@ -146,23 +146,24 @@ fully-functional VS Code text editor right inside your web browser.
 It's best to use an updated version
 of Chrome, Edge, or Firefox when using GitHub. In particular, Safari tends
 to show off its rough edges when using advanced web applications like
-<c>GitHub.dev</c>, so it's best to choose an alternative.
+<c>VSCode.dev/GitHub</c>, so it's best to choose an alternative.
             </p>
         </note>
         <p>
 You can create files, edit them, upload images, and do whatever you
-like at <c>GitHub.dev</c>. But this isn't your repository - it's just an
-example. So, we'll need a way to tell <c>GitHub.dev</c> we want to work on
+like at <c>VSCode.dev/GitHub</c>. But this isn't your repository - it's just an
+example. So, we'll need a way to tell <c>VSCode.dev/GitHub</c> we want to work on
 the repository we just made instead.
         </p>
         <note xml:id="opening-github-dev">
             <p>
-There are two very easy ways to access the <c>GitHub.dev</c> service.
+There are two very easy ways to access the <c>VSCode.dev/GitHub</c> service.
 The first is to just
 change the address of your repository from <c>GitHub.com</c> to
-<c>GitHub.dev</c> in your browser. For example, if your repository lives at
+<c>VSCode.dev/GitHub</c> in your browser. For example, if your repository lives at
 <c>https://github.com/YourUserName/YourGreatRepo</c>, you should visit
-<c>https://github.dev/YourUserName/YourGreatRepo</c>.
+<c>https://VSCode.dev/GitHub/YourUserName/YourGreatRepo</c> (or just
+<c>https://github.dev/YourUserName/YourGreatRepo</c> for short).
             </p>
             <p>
 The other trick is even fancier. When you are visiting
@@ -171,12 +172,12 @@ and not writing in a text box, press the period (<kbd>.</kbd>) key.
             </p>
         </note>
         <p>
-Either way, you should now have a <c>GitHub.dev</c> window where you can manage
+Either way, you should now have a <c>VSCode.dev/GitHub</c> window where you can manage
 all the files of your project. Using the <term>Explorer</term> sidebar
 (<xref ref="fig-explorer"/>), you can create
 new files, rename files, move files, upload files, and more. Selecting
 a file opens it, and lets you edit it as needed. Your changes are saved
-automatically in <c>GitHub.dev</c>, but they won't show up at <c>GitHub.com</c> just yet.
+automatically in <c>VSCode.dev/GitHub</c>, but they won't show up at <c>GitHub.com</c> just yet.
         </p>
         <figure xml:id="fig-explorer">
                 <image width="60%" source="screenshots/codespace-explorer-newfile.png"/>
@@ -204,21 +205,21 @@ you can easily see where exactly a change is made between each commit.)
         </p>
         <p>
 The idea is this: edit as you see fit, knowing that your files are being
-saved at <c>GitHub.dev</c> and won't be lost if you accidentally refresh your
+saved at <c>VSCode.dev/GitHub</c> and won't be lost if you accidentally refresh your
 web browser. However, you'll need to eventually commit those changes to
 the repository in order to share your work with anyone else, and to ensure
 that the work is preserved in the long term. The Source Control panel
 provides a place to write a <term>commit message</term>, a short
 phrase or sentence that summarizes the work you've done. (Writer's block?
-For now just type <q>learning GitHub.dev</q>.) Then once you click
+For now just type <q>learning VSCode.dev/GitHub</q>.) Then once you click
 the <q>Commit and Push</q> button, your work will be logged as a permanent
 commit to the repository.
         </p>
         <p>
 This is a good point to review your commit history again. You probably
 have three commits: the initial commit made when you created the repository,
 the <c>README.md</c> update you made using <c>GitHub.com</c>'s editing interface,
-and this more elaborate <c>GitHub.dev</c> commit involving possibly several files.
+and this more elaborate <c>VSCode.dev/GitHub</c> commit involving possibly several files.
 To visualize this history, you can go to the Insights/Network page
 described earlier, or click on the <q>3 commits</q> link
 from your <c>GitHub.com</c> repository

source/ch-website.ptx

@@ -18,7 +18,7 @@ to <xref ref="sec-using-a-template"/> to create a portfolio website
 without using HTML.)
         </p>
         <p>
-Use <c>GitHub.dev</c> (<xref ref="opening-github-dev"/>)
+Use <c>VSCode.dev/GitHub</c> (<xref ref="opening-github-dev"/>)
 to create three files in the root of a new or existing repository.
             <ul>
                 <li>
@@ -47,7 +47,7 @@ section, but for now add the following content:
 Download
 <dataurl source="git-branches.png"><c>git-branches.png</c></dataurl>
 (used for <xref ref="fig-git-branches"/>)
-and upload it to <c>GitHub.dev</c>.
+and upload it to <c>VSCode.dev/GitHub</c>.
                     </p>
                 </li>
             </ul>
@@ -94,7 +94,7 @@ or private.
                     </li>
                     <li>
                         <p>
-<c>GitHub.dev</c> is where you can make changes to your repository
+<c>VSCode.dev/GitHub</c> is where you can make changes to your repository
 through your web browser. This is private to you and you must commit
 and push your changes to the <c>GitHub.com</c> repository every so often.
 (See also <xref ref="sec-github-pages-codespace"/>.)
@@ -223,7 +223,7 @@ an orange dot (in progress), a green checkmark
 Now that you have the template website hosted by GitHub Pages, you of course
 will want to customize it to yourself. For this book, I'll get you started by
 handling a few of the obvious first steps, assuming you're
-using the <c>GitHub.dev</c> service (<xref ref="opening-github-dev"/>).
+using the <c>VSCode.dev/GitHub</c> service (<xref ref="opening-github-dev"/>).
             </p>
         </introduction>
         <subsection xml:id="subsec-posts-and-pages-config">
@@ -374,7 +374,7 @@ your changes
 (<xref ref="note-commit-sync"/>).
     </p>
     <p>
-Personally, I use <c>GitHub.dev</c> (or even just the
+Personally, I use <c>VSCode.dev/GitHub</c> (or even just the
 <c>GitHub.com</c> edit button) rather than a full
 Codespace when adding a quick post or making a quick edit on
 many of my GitHub Pages websites. But the Codespace option is very