javascript document.write '</div>', not '<\/div>'

At least htmltidy complains, and AFAIK, that document.write() should use '<\/div>' instead of '</div>'. I can not paste the patch directly (2 lines changed but the system says it's suspicious even within <code> tags) so I'll attach it.