It seems more an inconsistency between input and output. Indeed, the HTML5 regards (almost) anything after </html> as part of the end of the body, so, here this would be the newline character. But in such a case, a newline character shouldn't be added after </html> in the output when using the string output format. An alternate view is to regard the ending newline not as part of the data (the goal being to have a POSIX text file in some cases).
-- Vincent Lefèvre <vinc...@vinc17.net> - Web: <https://www.vinc17.net/> 100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/> Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)
