summaryrefslogtreecommitdiff
path: root/doc/makefile
diff options
context:
space:
mode:
Diffstat (limited to 'doc/makefile')
-rw-r--r--doc/makefile18
1 files changed, 12 insertions, 6 deletions
diff --git a/doc/makefile b/doc/makefile
index a192e00..6f48746 100644
--- a/doc/makefile
+++ b/doc/makefile
@@ -14,18 +14,24 @@ port ?= 8082
clean:
rm -f $(output_dir)/*.html
+ rm -f *.info
web:
rm -f $(output_dir)/*.html
texi2html --output=$(output_dir) \
- --split=chapter \
- --noheader \
- --nonumber-section \
- --init-file=$(top_srcdir)/doc/site.conf \
- --top-file=index.html \
- $(top_srcdir)/doc/web.texi
+ --split=chapter \
+ --noheader \
+ --nonumber-section \
+ --init-file=$(top_srcdir)/doc/site.conf \
+ --top-file=index.html \
+ $(top_srcdir)/doc/web.texi
cp $(top_srcdir)/doc/geiser.css ${output_dir}
cp -r $(top_srcdir)/doc/img ${output_dir}
http: web
cd $(output_dir) && python -m http.server $(port)
+
+info: geiser.info dir
+
+%.info: %.texi
+ makeinfo --no-split $< -o $@