document.getElementById("pvtitle").textContent = "Exploring:";
current_display_line.start_display_move_num = 0;
display_lines.push(current_display_line);
- document.getElementById("pv").append(print_pv(display_lines.length - 1, null)); // FIXME
+ document.getElementById("pv").replaceChildren(print_pv(display_lines.length - 1, null)); // FIXME
display_line_num = display_lines.length - 1;
// Clear out the PV, so it's not selected by anything later.