c73767a0bc
This patch makes `HTMLOutputFormat` correctly escape all < and > characters that occur in source code. Otherwise, a web browser rendering the resulting HTML will interpret those characters as tags.