function fontSizeChange( s ){
document.getElementById("pagebody").style.fontSize=s + "%";
}