Make timeit.bat handle some non-US locales better

timeit.bat assumed the decimal separator was a period. Sometimes
it's a comma.

Change-Id: Id8d04f980907dda0d80af96be8568b1704b61399
Reviewed-on: https://chromium-review.googlesource.com/844322
Commit-Queue: Daniel Bratell <bratell@opera.com>
Reviewed-by: Bruce Dawson <brucedawson@chromium.org>
Cr-Original-Commit-Position: refs/heads/master@{#526285}
Cr-Mirrored-From: https://chromium.googlesource.com/chromium/src
Cr-Mirrored-Commit: 81bbbfa8a4b82ce956c8b1e77d4ea67869e7c895
diff --git a/subtract_time.py b/subtract_time.py
index 4e1559b..e11c6bf 100644
--- a/subtract_time.py
+++ b/subtract_time.py
@@ -3,7 +3,7 @@
 # found in the LICENSE file.
 
 """
-This script converts to %time% compatible strings passed to it into seconds,
+This script converts two %time% compatible strings passed to it into seconds,
 subtracts them, and prints the difference. That's it. It's used by timeit.bat.
 """
 
@@ -11,8 +11,9 @@
 import sys
 
 def ParseTime(time_string):
-  # Time looks like 15:19:30.32
-  match = re.match("(.*):(.*):(.*)\.(.*)", time_string)
+  # Time looks like 15:19:30.32 or 15:19:30,32 depending on locale
+  # (and there might be other variants as well)
+  match = re.match("(.*):(.*):(.*)[\.,](.*)", time_string)
   hours, minutes, seconds, fraction = map(int, match.groups())
   return hours * 3600 + minutes * 60 + seconds + fraction * .01