-
Notifications
You must be signed in to change notification settings - Fork 34
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Suggestion: Rename repository to purescript.org #155
Comments
I believe it has to be named this for the hosting setup to work, as it's served by GitHub pages. |
Do you have documentation for this claim at hand? E.g. I have this repository with a different name schema and am using github pages: It's using CI and a github action, but I think this is because there's a build step involved. And there are random guides not mentioning the necessity to choose a specific name. It might be that purescript.github.io might be coupled to the repo name, which is a valid concern, but my assumption is that it's not necessary in general. Github itself would serve the page under |
You're probably right - I've only followed the workflow for a username/org site before and it dictates you name the repo a particular way. I thought you could only set the custom domain at that level, and then subsequent projects would be served from |
I think this change should be done. I also found it hard when I first tried to figure this out. |
Not a big deal, but it would have helped me figuring out where the source code of the official website is hosted, if the name would have been
purescript.org
, and it's probably slightly better. As far as I know renaming a repository will not break any cases where the old name is used, because it'll continue to work.The text was updated successfully, but these errors were encountered: