<?php
/**
 * Fonction globale récupérant le microtime de la machine en format float.
 * @return float	Valeur courante du microtime() de la machine en format décimal
 */
function getmicrotime(){
	list($usec, $sec) = explode (' ', microtime());
	return ( (float)$sec + (float)$usec );
}

if ( LOG_BENCH != 'NONE'){
	require_once ('Benchmark/Timer.php');
	$timer = new Benchmark_Timer();
	$timer->start();
	$timer->setMarker('Debut du script (prepend.php)');
}