', $_SERVER['REQUEST_URI'])) // $source = file_get_contents('global_ie.js'); //else $source = file_get_contents('header_global.js'); $source = $source.file_get_contents('global.js'); //Affichage de la source echo $source; ?>