// JavaScript Document

function changeCharaSize (size) {
	document.getElementById ("mainContent") .style.fontSize = size + 'px';
}