function doZoom(size){
	try{
		document.getElementById('zoom').style.fontSize=size+'px';
	}catch(e){}
}