function hover_link(id) {
	document.getElementById(id).className = "underlined";
}

function dehover_link(id) {
	document.getElementById(id).className = "";
}