From f59403fbc349320e2bfba711bd55128e4bde0517 Mon Sep 17 00:00:00 2001
From: Frédéric Chapoton
Date: Mon, 4 Mar 2019 21:08:21 +0100
Subject: remove unused import of os

found by lgtm

https://lgtm.com/projects/g/coq/coq/---
 tools/TimeFileMaker.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tools/TimeFileMaker.py')

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
-- 
cgit v1.2.3