script to get the ping time to a domain host

ping.php

<?php

$domain = 'http://mona.lu';

echo getPingTime($domain);

function getPingTime($domain) {
    $domain = parse_url($domain, PHP_URL_HOST);
    exec("ping -c 1 " . $domain . " | head -n 2 | tail -n 1 | awk '{print $7}'", $ping_time);
    return $ping_time[0];
}