Paul Melnikow authored Apr 20, 2017 and Thaddée Tyl committed Apr 25, 2017

- Build index.html at deploy time
- Update corresponding documentation references
- Since index.html is untracked, git add needs -f
- Clarify gh-pages generated commit message
- Improve Makefile dependencies related to website generation

As discussed in #936, tracking the index.html causes makes PRs longer / noisier
and causes extra merge conflicts. More importantly, it causes contributors to
inadvertently edit the wrong file, which causes extra work (#949) or
contributions to be lost (#898).

Since there's no need for index.html in development (everything uses try.html) a
logical solution is to generate and commit the index.html at deploy time.

Recording compiled or generated files in a deploy commit is a reasonable
practice for git-based deploys (Heroku, gh-pages, and others).

The old version of this was slightly "unsafe" for my taste, in that it depended
on the local copy of gh-pages (if it existed) and master. The new version just
replaces gh-pages with master + the new commit.

Closes #936.

Fixes #954 (the PR).