Function undo

src/functions.js:2199–2213

()

	}
}
function undo() {
	if (undos.length < 1) { return false; }

	redos.push(current_history_node);
	let target_history_node = undos.pop();

	while (target_history_node.soft && undos.length) {
		redos.push(target_history_node);
		target_history_node = undos.pop();
	}

	go_to_history_node(target_history_node);

	return true;
}

// @TODO: use Clippy.js instead for potentially annoying tips
/** @type {OSGUI$Window} */