Extend MaxTime format to support milliseconds and plain millisecond integers

[mariofuest]

The spec currently documents MaxTime for bestmove time as hh:mm:ss. I'd like to propose two additional formats:

• hh:mm:ss.MMM — dot-separated milliseconds, e.g. 00:00:01.500 for 1.5 seconds. The dot follows the ISO 8601 convention for sub-second precision.
• M+ — a plain integer interpreted as milliseconds, e.g. 1000 for 1 second.

The point is that the minimum of 1s may be rather large.

The old format hh:mm:ss should continue to work, of course.