Problem with fix for bug #31672

Guys, I'd like to revert the fix for bug #31672 ("</script> is not considered closing tag if preceded by one-line comment"). While theoretically correct, I'd rather resolve it by fixing the docs. The reason is simple - unlike ?> and %>, the string "</script>" is very much likely to appear inside one line comments: // print "<script>foo</script>"; That suddenly fails. That's probably the reason we didn't implement it in the first place. Any objections to reverting this fix? Zeev