diff options
| author | Frédéric Chapoton | 2019-03-04 21:08:21 +0100 |
|---|---|---|
| committer | GitHub | 2019-03-04 21:08:21 +0100 |
| commit | f59403fbc349320e2bfba711bd55128e4bde0517 (patch) | |
| tree | e4879218b0b77e81e718ae3b85e0d6b5b5184d1f /tools | |
| parent | 78b3b96d1ca2c2811cee2ca4202c154177d943a2 (diff) | |
remove unused import of os
found by lgtm
https://lgtm.com/projects/g/coq/coq/
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 |