GitHub-Dark
GitHub-Dark copied to clipboard
GitHub Codespaces
GitHub's new feature codespaces brings function to access to local server via https://<randomized id>.apps.codespaces.githubusercontent.com/
. Therefore, We need to exclude it from apply list.
- Browser: Brave Browser
- Operating System: Windows 10 Pro 2004
-
Link to page with the issue:
https://<randomized id>.apps.codespaces.githubusercontent.com/
-
Screenshot:
You can simply just use Stylus feature to do the job for you without us needing to do anything special.
So the job really is already done for the 1% of users coming across whatever the issue is.
I guess we could exclude it our the regex if it really looks that bad. Does it come with a built in dark theme?
Codespaces is just VS Code in the browser, it's fully themeable just like the desktop version. @tomocrafter can correct me on this, but I believe what they're doing is opening a port from the VM to run their application through and it's being themed with GHD when it shouldn't be.
Can someone with access to Codespaces test if replacing
domain("githubusercontent.com")
with
regexp("^https?://(?:(?!codespaces).)*githubusercontent\\.com.*$")
works?
https://regex101.com/r/uA8HYl/2
The regex is just a stop gap, via stylus you can ignore some pages anyway as I detailed above.
If that random part of the hostname changes often, it would be a burden.
There's 3 urls I'm seeing when using port forwarding.
The first initiates authentication using the format https://github.com/codespaces/auth/{guid}?port={forwarded-port}&cid=...
. This is themed but only shows for a split second in a new window so I couldn't get a copy of the html/css it's using.
The second is the auth redirect which uses https://auth.apps.codespaces.githubusercontent.com/authenticate-codespace/...
. This does have a small loading animation but isn't themed.
The third url is the one that your application loads with. The subdomain for this one changes for each vm and forwarded port (if you forward 10 ports you get 10 different subdomains). These use the format https://{guid}-{forwarded-port}.apps.codespaces.githubusercontent.com/
.
Replacing both occurrences of domain("githubusercontent.com")
removes GHD as you'd expect.
Looks like it is now https://$USERNAME-$REPO-$HASH.github.dev/
, so *.github.dev
should do the trick.
github.dev
is where the IDE lives now, but port forwarding still goes through https://7f2c8767-c59c-43b5-9208-ea63ef183aec-8080.apps.codespaces.githubusercontent.com/
, at least for one of my existing environments (created July 28th), not sure if new ones are different.