diff -r 56e8c0a3fe9a -r 45fc36beb0aa make/Docs.gmk --- 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), \