diff options
| author | Maxime Dénès | 2017-10-09 15:46:32 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-09 15:46:32 +0200 |
| commit | ef5aa53e49769fc3c9b31c224ba110b8a059e847 (patch) | |
| tree | ac12afd91d0fc746eb9d0b0127d9128739f7873a | |
| parent | 82ebd162a6b31d1056eb630b9805cdcb83b8fa04 (diff) | |
| parent | 9abc3dcc7933091d6c31ff9896996b57654c5ebd (diff) | |
Merge PR #1132: TimeFileMaker.py: Allow trailing spaces
| -rw-r--r-- | tools/TimeFileMaker.py | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index a207c2171b..7298ef5e8e 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -28,10 +28,10 @@ def get_times(file_name): else: with open(file_name, 'r') as f: lines = f.read() - reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)$', re.MULTILINE) + reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) times = reg.findall(lines) if all(time in ('0.00', '0.01') for name, time in times): - reg = re.compile(r'^([^\s]*) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)$', re.MULTILINE) + reg = re.compile(r'^([^\s]*) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) times = reg.findall(lines) if all(STRIP_REG.search(name.strip()) for name, time in times): times = tuple((STRIP_REG.sub(STRIP_REP, name.strip()), time) for name, time in times) |