
It was gone, turns out, because it consisted of non-breaking spaces (ASCII 160) instead of standard spaces (ASCII 32), and I set my editor to remove these chars (Options > File > Miscellaneous > Remove any characters...) on save. Now, why would anybody need to use non-breaking spaces for indentation, if the whole clip is surrounded by <pre></pre> tags? Someone who wrote code for "Copy as HTML (black and white)"

And while I am at it: there's no need to surround indentation with <span></span>. Also "style" attribute value for <pre> tag instead of
Code: Select all
font-family: Fira Code;font-size: 12 pt;
Code: Select all
font-family: monospace;