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>
diff --git a/docs/Makefile b/Makefile
similarity index 61%
rename from docs/Makefile
rename to Makefile
index 0f38bfa..082a598 100644
--- a/docs/Makefile
+++ b/Makefile
@@ -3,10 +3,10 @@
default: all
all_markdown = \
- psa/index.md \
- psa/accel/index.md \
- psa/entropy/index.md \
- psa/se/index.md \
+ docs/psa/index.md \
+ docs/psa/accel/index.md \
+ docs/psa/entropy/index.md \
+ docs/psa/se/index.md \
# This line is intentionally left blank
html: $(all_markdown:.md=.html)