diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/makefile | 18 |
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 $@ |