Fix #8152: handle \0 lines as empty (#8348)

Browsers render lines with just \0 chars as zero-height. Treat them as
empty lines instead

Implementing the suggestion raised in the issue discussion.
This commit is contained in:
Ofek
2025-12-20 14:07:14 +02:00
committed by GitHub
parent a7038e1263
commit 427bb145e1

View File

@@ -537,7 +537,8 @@ export class Executor extends Pane<ExecutorState> {
): JQuery<HTMLElement> { ): JQuery<HTMLElement> {
const outElem = $('<pre class="card execution-stdoutstderr"></pre>').appendTo(element); const outElem = $('<pre class="card execution-stdoutstderr"></pre>').appendTo(element);
output.forEach(obj => { output.forEach(obj => {
if (obj.text === '') { // Bug #8152: output lines with only null characters should be rendered as empty lines
if (obj.text === '' || (obj.text.includes('\x00') && obj.text.replace(/\x00/g, '') === '')) {
this.addCompilerOutputLine('<br/>', outElem, undefined, undefined, false, null); this.addCompilerOutputLine('<br/>', outElem, undefined, undefined, false, null);
} else { } else {
const lineNumber = obj.tag ? obj.tag.line : obj.line; const lineNumber = obj.tag ? obj.tag.line : obj.line;