Updating GitHub Pages

In order to update the documentation on GitHub Pages, do the following:

1. Build the DAPS documentation:

    daps -vv -d DC-daps-all package-html
   

2. Change into the gh-pages branch:

    git checkout gh-pages
   

3. Unpack the tarball from daps-all/package/html/ into the doc/ directory.

4. If your page doesn't show up, go to the Settings page. Watch for error messages in the GitHub Pages section.