(.*?)<\/arch>/', $s, $m))
echo "| ", he($m[1]), " | ";
else
echo "— | \n";
echo "\n";
$then = filemtime($file);
echo "", strftime("%b-%d %H:%M", $then), " | \n";
$dm = floor((time() - $then) / 60);
echo "${dm}m | \n";
}
function p_host($work_dir, $host)
{
ksort($host["worker"]);
foreach ($host["worker"] as $id => $state) {
echo "| ", he($id), " | \n";
$f = "$work_dir/building/".$host["arch"].":".$host["name"]."_$id";
if (strcmp($state, "") == 0)
echo "(idle) | \n";
else if (!is_file($f))
echo "(error reading ", he($f), ") | \n";
else
p_worker($f);
echo "
\n";
}
}
function p_workgroup($work_dir)
{
$res = array();
$dlist = glob("$work_dir/*/*");
foreach ($dlist as &$e) {
if (!preg_match('/(\w+)\/(\w+):(\S+)_(\d+)$/', $e, $m))
continue;
list(, $state, $arch, $host, $id) = $m;
$nick = preg_replace('/^(.*?)\..*/', '$1', $host);
$res[$host]["name"] = $host;
$res[$host]["nick"] = $nick;
$res[$host]["arch"] = $arch;
$res[$host]["worker"][$id] =
strcmp($state, "idle") == 0 ? "" : $id;
}
asort($res);
foreach ($res as $host) {
echo "", he($host["nick"]), " (", he($host["arch"]), ")
\n\n";
p_header();
p_host($work_dir, $host);
p_footer();
}
}
date_default_timezone_set("Europe/Berlin");
p_counts("/srv/obs/jobs");
p_workgroup("/srv/obs/workers");
?>