purescript.github.io icon indicating copy to clipboard operation
purescript.github.io copied to clipboard

Suggestion: Rename repository to purescript.org

Open andys8 opened this issue 3 years ago • 4 comments

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.

andys8 avatar Feb 03 '23 12:02 andys8

I believe it has to be named this for the hosting setup to work, as it's served by GitHub pages.

garyb avatar Feb 03 '23 12:02 garyb

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: https://github.com/andys8/type-signature-com/deployments/activity_log?environment=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 purescript.github.io/<repository-name>, which would be https://purescript.github.io/purescript.github.io right now. The custom domain https://purescript.org should always work.

andys8 avatar Feb 03 '23 13:02 andys8

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 http://custom-domain/whatever-project, but I can't see anything that states that for sure (it's just that the docs only give the example for user/org site that I've seen), so seems likely it should be possible to set a custom domain on a project site too.

garyb avatar Feb 06 '23 13:02 garyb

I think this change should be done. I also found it hard when I first tried to figure this out.

JordanMartinez avatar Feb 07 '23 02:02 JordanMartinez