function setFontSize(divId, size) {
   el = document.getElementById(divId);
   el.style.fontSize = size+"px";
}