Warning in admin/tool/crawler/index.php float to int conversion

[rrusso]

Change line 159

$duration = sprintf('%02d:%02d:%02d', $delta / 60 / 60, $delta / 60 % 60, $delta % 60);

to

$duration = sprintf('%02d:%02d:%02d', $delta / 60 / 60, intval($delta / 60) % 60, $delta % 60);