| commit | db82c58d1b890b6d2265542d76c0cc4bbf20a0c0 | [log] [tgz] |
|---|---|---|
| author | Gilles Peskine <Gilles.Peskine@arm.com> | Mon Jan 18 20:20:48 2021 +0100 |
| committer | Gilles Peskine <Gilles.Peskine@arm.com> | Mon Jan 18 20:20:48 2021 +0100 |
| tree | 90340c00b594fe7a43be0060335f7f3561e9d730 | |
| parent | 70d91d931d096236b3844298d51ca4feeab29d09 [diff] |
Move Makefile out of docs/ GitHub Pages serves the files under `docs`. There's no reason to serve `Makefile`, which is only there to build a few generated files. So move it out. Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com>