![]() - 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). |
||
---|---|---|
.. | ||
TUTORIAL.md | ||
users.md |