// JavaScript Document
function changeFontSize(size ) {
	if(document.getElementById('art_body'))
		document.getElementById('art_body').style.fontSize = size + 'px';
}