diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile.local | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/Makefile.local b/doc/Makefile.local index 16459e35..eec9c228 100644 --- a/doc/Makefile.local +++ b/doc/Makefile.local @@ -37,6 +37,10 @@ INFO_INFO_FILES := $(INFO_TEXI_FILES:.texi=.info) %.gz: % rm -f $@ && gzip --stdout $^ > $@ +ifeq ($(WITH_EMACS),1) +sphinx-html sphinx-texinfo: docstring.stamp +endif + sphinx-html: $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(DOCBUILDDIR)/html |