diff options
| author | Emilio Jesus Gallego Arias | 2019-03-15 19:19:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-15 19:19:41 +0100 |
| commit | 2f4a2a7adfbf4831ee03310e9f918c7d49c8d991 (patch) | |
| tree | 1f485593892029b218e7ac046787d4ecd39250ab /tools | |
| parent | ed275fd5eb8b11003f8904010d853d2bd568db79 (diff) | |
| parent | f59403fbc349320e2bfba711bd55128e4bde0517 (diff) | |
Merge PR #9694: remove unused import of os
Reviewed-by: JasonGross
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/TimeFileMaker.py | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 8564aeff64..854dd25b75 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -2,7 +2,8 @@ from __future__ import with_statement from __future__ import division from __future__ import unicode_literals from __future__ import print_function -import os, sys, re +import sys +import re from io import open # This script parses the output of `make TIMED=1` into a dictionary |