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