make/Docs.gmk
changeset 55651 45fc36beb0aa
parent 55488 d3e45bd166dc
child 55673 0bf678dd8951
--- a/make/Docs.gmk	Thu Jul 11 08:19:56 2019 +0900
+++ b/make/Docs.gmk	Wed Jul 10 16:23:59 2019 -0700
@@ -626,7 +626,7 @@
             FILTER := $(PANDOC_HTML_MANPAGE_FILTER), \
             CSS := $(GLOBAL_SPECS_DEFAULT_CSS_FILE), \
             REPLACEMENTS := @@VERSION_SHORT@@ => $(VERSION_SHORT), \
-            OPTIONS := -V include-before='$(SPECS_TOP)' -V include-after='$(SPECS_BOTTOM_1)', \
+            OPTIONS := --toc -V include-before='$(SPECS_TOP)' -V include-after='$(SPECS_BOTTOM_1)', \
             POST_PROCESS := $(TOOL_FIXUPPANDOC), \
             EXTRA_DEPS := $(PANDOC_HTML_MANPAGE_FILTER) \
                 $(PANDOC_HTML_MANPAGE_FILTER_JAVASCRIPT), \