gustafn
committed
on 03 Nov 21
make sure, the end_clock is always an integer (as required by "clock format")