Avoid `git pull`

`git pull` is sometimes frowned upon because you might make a mess with it. It should be replaced with a workflow like
```bash
git fetch
git diff origin/<branch name>
git rebase/merge origin/<branch name>
```
If it's feasible (in the lecture context) to consequently change that everywhere is debatable but it should at least be advertised upon first use of `git pull`.