[gecode-users] printing of time in script.cpp

[Jan Kelbel]

Hi,

I found some non-correct behavior in function
void stop(Support::Timer& timer, std::ostream& os)
lines 57 to 67 in release 3.7.1 in file gecode\driver\script.cpp

When for example (o_hour > 0) and (o_min == 0), then the result of the 
output is o_hour:o_sec.o_msec, and the minute part is skipped.

Possibly, the lines 59 and 60 can be replaced by:

if (o_hour) {
   os << o_hour << ":";
   if (0 == o_min) {
     os << "00:";
     os.width(2); os.fill('0');
   }
}

Cheers,
	Jan