diff options
| author | rsiddharth <s@ricketyspace.net> | 2016-07-11 02:03:20 +0000 |
|---|---|---|
| committer | rsiddharth <s@ricketyspace.net> | 2016-07-11 02:03:20 +0000 |
| commit | 2ea195dfbc4da32cbf729fe4f4515849e4ebbd97 (patch) | |
| tree | 32ec668c3ea4057a79dff527f2eb208ba259b996 /.gitignore | |
| parent | 8845d6ed54c93957227c34b22c909b475ed38baf (diff) | |
add stuff to generate docs.
* .gitignore: ignore docs/_build directory.
* Makefile (docs, push-docs, docs-clean): new targets.
* docs/Makefile: new file
* docs/assets/includes/header.html: new file.
* docs/assets/includes/footer.html: new file.
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -1 +1,2 @@ -*~
\ No newline at end of file +*~ +docs/_build/
\ No newline at end of file |