Hide paragraph terminator at the end of headings on html export (#4194).
Authored by: jplang 2009-11-11
Parent: [r3025]
Child: [r3027]
