/*
redimentionner la taille de la police
*/
function text_size(new_size) {
var d = document.getElementById('content');
if (d) {d.style.fontSize=new_size+'em';}
}