fix VSCode.dev in the other files

Author: StevenClontz

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-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