Do not commit the index.html file.

[niccokunzmann]

Context: The index.html file is generated from the try.html file with the command make website.
Problem: This cases merge conflicts for generated code, makes commits bigger, duplicates code to maintain.

Solution:

• Clarify if index.html should be tracked by git at all
• remove the description in the tutorial that it should be committed
• Add the building of the index.html page to the deploy script source
• Document:
  • maybe: make travis fail if the last commit changes the index.html file as a warning to contributors
  • Change the README and other documentation files to document that this file does not need to be touched

[paulmelnikow]

We could run make website at deploy time, and push the updated index.html to master.

It's a good question you raise. Should it be tracked at all? We could consider removing it from tracking in master. It would have to be committed to the gh-pages branch, though that could be done on a detached head as part of the deploy scripts, which would mean most contributors would never see it.

There's a real advantage to that: removing it from tracking in master would take the chance of confusion to zero.

I don't know whether the index.html is needed anywhere else. Should find that out.

[paulmelnikow]

This happened again in #949.

index.html does not seem to be needed for development. I'd suggest we modify the deploy-gh-pages target to build index.html and commit it, before the force-push to gh-pages.

[paulmelnikow]

Opened a PR: #954.