+function format_time(t)
+{
+ const ms = t % 1000 + '';
+ t = Math.floor(t / 1000);
+ const sec = t % 60 + '';
+ t = Math.floor(t / 60);
+ const min = t % 60 + '';
+ const hour = Math.floor(t / 60) + '';
+ return hour + ':' + min.padStart(2, '0') + ':' + sec.padStart(2, '0') + '.' + ms.padStart(3, '0');
+}
+