Setting up extrinsic branch

This commit is contained in:
wadler 2019-01-11 09:10:56 +00:00
parent 4a80d4e0e3
commit 4896989ba2
2 changed files with 17 additions and 1 deletions

View file

@ -8,6 +8,21 @@ permalink: /Notes/
<https://analytics.google.com/analytics/web/>
## Git commands
Git commands to create a branch and pull request
git help <command> -- get help on <command>
git branch -- list all branches
git branch <name> -- create new local branch <name>
git checkout <name> -- make <name> the current branch
git merge <name> -- merge branch <name> into current branch
git push origin <name> -- make local branch <name> into remote
git rebase <base> -- merge branch <base> into current branch
On website, use pulldown menu to swith branch and then
click "new pull request" button.
## Suggestion from Conor for Inference
Conor McBride <conor.mcbride@strath.ac.uk>

View file

@ -171,7 +171,8 @@ configuration file at `~/.emacs`, if you have the mentioned fonts available:
## Markdown
The book is written in [Kramdown Markdown](https://kramdown.gettalong.org/syntax.html).
The book is written in
[Kramdown Markdown](https://kramdown.gettalong.org/syntax.html).
## Travis Continuous Integration