bless cargo miri doctest execution

Author: RalfJung

src/tools/miri/test-cargo-miri/run-test.py

@@ -37,7 +37,7 @@ def cargo_miri(cmd, quiet = True, targets = None):
 
 def normalize_stdout(str):
     str = str.replace("src\\", "src/") # normalize paths across platforms
-    str = re.sub("finished in \\d+\\.\\d\\ds", "finished in $TIME", str) # the time keeps changing, obviously
+    str = re.sub("\\b\\d+\\.\\d+s\\b", "$TIME", str) # the time keeps changing, obviously
     return str
 
 def check_output(actual, path, name):

src/tools/miri/test-cargo-miri/test.default.stdout.ref

@@ -14,3 +14,4 @@ running 5 tests
 .....
 test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in $TIME
 
+all doctests ran in $TIME; merged doctests compilation took $TIME

src/tools/miri/test-cargo-miri/test.filter.stdout.ref

@@ -15,3 +15,4 @@ running 0 tests
 
 test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 5 filtered out; finished in $TIME
 
+all doctests ran in $TIME; merged doctests compilation took $TIME

src/tools/miri/test-cargo-miri/test.multiple_targets.stdout.ref

@@ -25,8 +25,10 @@ running 5 tests
 .....
 test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in $TIME
 
+all doctests ran in $TIME; merged doctests compilation took $TIME
 
 running 5 tests
 .....
 test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in $TIME
 
+all doctests ran in $TIME; merged doctests compilation took $TIME