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 /dev/ci | |
| parent | 78b3b96d1ca2c2811cee2ca4202c154177d943a2 (diff) | |
remove unused import of os
found by lgtm
https://lgtm.com/projects/g/coq/coq/
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions