Replace Makefile with redo

diff --git a/doc/.gitignore b/doc/.gitignore
index e35d8850c9688b1ce82711694692cc574a799396..28e3f58b68610968be2635a34b0c0cdfd43baae7 100644 (file)
--- a/doc/.gitignore
+++ b/doc/.gitignore
@@ -1 +1,2 @@
 _build
+build.log

diff --git a/doc/Makefile b/doc/Makefile
deleted file mode 100644 (file)
index 2edea2b..0000000
--- a/doc/Makefile
+++ /dev/null
@@ -1,2 +0,0 @@
-html:
-       python -msphinx . _build/html

diff --git a/doc/build.log.do b/doc/build.log.do
new file mode 100644 (file)
index 0000000..2b9c5e9
--- /dev/null
+++ b/doc/build.log.do
@@ -0,0 +1,7 @@
+rm -fr _build
+html=_build/html
+PYTHONPATH=.. ${PYTHON:=python} -msphinx . $html
+cp -r download $html
+rm -r $html/.doctrees $html/.buildinfo
+find $html -type d -exec chmod 755 {} \;
+find $html -type f -exec chmod 644 {} \;