RFR: JDK-8214720 Add pandoc filter to improve html man page output

[Erik Joelsson]

Looks good.

/Erik

On 2018-12-03 09:42, Magnus Ihse Bursie wrote:
> The html output of man pages looks weird due to the metadata header 
> required by pandoc to generate proper man pages. We should add a 
> pandoc filter for html output as well.
>
> The actual javascript filter implementation was graciously provided to 
> me by Jon.
>
> Bug: https://bugs.openjdk.java.net/browse/JDK-8214720
> WebRev: 
> http://cr.openjdk.java.net/~ihse/JDK-8214720-pandoc-filter-for-html-manpages/webrev.01
>
> /Magnus