Skip to content

GitHub Workflow

Paul Sheridan edited this page Jan 17, 2025 · 2 revisions

This is a very much work in progress.

Permanent branch names follow the naming convention dev-*. Currently, there are two such permanent branches:

  • dev-themes: This is a branch for updating theme files (i.e., .th.txt extension files). Example work: coining new themes, improving existing themes, and deprecating old themes.
  • dev-stories: This is a branch for updating exiting story files (i.e., .st.txt extension files). Example work: improving theme motivations, improving story entries, adding new themes to existing stories, and deleting themes from stories.

When merging a pull request from a permanent branch, choose the Create a merge commit option.

merge-pull-request-options

Choose the Squash and merge option when merging pull requests from feature branches.

Thematically annotating a collection of stories for the first time is a common task. This is done by creating a new branch:

git checkout -b mycollection
git push --set-upstream origin mycollection

Annotate the stories on that branch. When completed, submit a pull request. The branch should be deleted after the pull requested is accepted.