html-encode-chars.patch
