Closed twardoch closed 3 years ago
No, no! That's not what it's about. Because this is hosted as a Github "user page", gh-pages needs the HTML to be in the master
branch. So that can't be renamed. The source
branch is the markup that we edit to produce the HTML, and that source is in XML.
I may be in a minority but I think having it in XML is pretty useful for a variety of reasons: repurposing for different output formats, and being able to programmatic select portions of the output (e.g. with/without test suites; with/without sample implementation; with explanatory notes or just the bare formal spec).
Github "user page", gh-pages needs the HTML to be in the master branch. So that can't be renamed.
It's possible in the GitHub Repository settings to change the branch GitHub Pages uses.
The options are limited, but you can make a gh-pages
branch and use it, which would be less confusing than master.
You can also use a docs directory in the master branch. Here are the GH Pages configuration docs.
In general, this is is true. But if it is a page for your user account (in this case commontypestandard.github.io
), you must use the master branch.
I suppose the obvious step would be to rename the repo so it isn't the user page; that should enable us to still host it on commontype.org. I'll see if I can work it out.
OK, I think that's got it - renamed to "commontype" (I feel a bit weird about standard vs. specification anyway), moved everything from old-master
to docs/
on new master, merged source into master, and got rid of source branch.
OK, I fixed some links in readme, will fix more
I’m confused about the roles of the
master
andsource
branches. I propose to put the “old” AOTS stuff into a branch namedoriginal
orarchive
, and forget about it once and for all, and in the working branch (master
), keep only Markdown files, the stuff to build the website, but forget about the Java and old XML stuff. @simoncozens agree?