--- old/make/ToolsJdk.gmk	2018-11-27 11:21:29.965920428 +0100
+++ new/make/ToolsJdk.gmk	2018-11-27 11:21:29.577920431 +0100
@@ -116,4 +116,10 @@
 
 ##########################################################################################
 
+# Executable javascript filter for man page generation using pandoc.
+
+PANDOC_FILTER := $(BUILDTOOLS_OUTPUTDIR)/manpages/pandoc-manpage-filter
+
+##########################################################################################
+
 endif # _TOOLS_GMK