// $id:$
function JumpMenu(loc) {
	if(loc != "") {
		window.location.href=loc;
	}
}
// EOF