Added support to edit page links for github.dev (web editor) URLs.

paulhibbitts · Aug 27, 2023 · 94dd37b · 94dd37b
1 parent 4cb49e1
commit 94dd37b
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/docs/index.html b/docs/index.html
@@ -872,7 +872,11 @@
                       if (currentBasePath.includes("githubusercontent.com") && (existingEditThisPageLink.substr(existingEditThisPageLink.length - fileExt.length) == fileExt)) {
                         var editThisPageLink = '';
                         editThisPageLink = decodeURIComponent(currentBasePath);
-                        editThisPageLink = editThisPageLink.replace('raw.githubusercontent.com', 'github.com');
+                        if (existingEditThisPageLink.includes('github.dev')) {
+                          editThisPageLink = editThisPageLink.replace('raw.githubusercontent.com', 'github.dev');
+                        } else {
+                          editThisPageLink = editThisPageLink.replace('raw.githubusercontent.com', 'github.com');
+                        }
                         editThisPageLink = editThisPageLink.replace(/\/main/, '/blob/main');
                         editThisPageLink = editThisPageLink.replace(/\/master/, '/blob/master');
                         //console.log(lastSegment);