add a function to format a time into a duration. Can't use date() because 0 doesn't give us 00:00:00 it gives 19:00:00

web/includes/functions.php

@@ -2446,4 +2446,8 @@ function getAffectedIds( $name ) {
 	return $ids;
 }
 
+function format_duration($time, $separator=':') {
+  return sprintf('%02d%s%02d%s%02d', floor($time/3600), $separator, ($time/60)%60, $separator, $time%60);
+}
+
 ?>