<!--
function changeCharaSize(size){
	document.getElementsByTagName("body")[0].style.fontSize=size+'px'; 
}
//-->