function to get the generation page time

[astkboy2008]

today i got very nice php function from jooria
its give you the generation page time
the function:
function gen_time() {
static $time;
if($time== 0){
$time= microtime(true);
}else{
return (string)(microtime(true)-$time);
}
}
how you can use:
gentime();

# your source code here

echo 'Generated in '.gentime().' seconds.'
the snippet (http://www.jooria.com/snippets?snippet=114)