Make publishing easier

[fdedden]

Publishing the generated .html files after running make is tedious, as they have to be moved to the master branch. Moving them is not as simple as git add . && git checkout master, as this will create merge conflicts.

A proper solution needs to be found, but for now:

git add .
git stash
git checkout $branch
git checkout --theirs stash -- .
git stash drop
git reset .
git clean -df
git clean -df

suffices.

This leaves us with all the changes ready for adding and committing in master.