diff options
author | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-07-07 09:19:13 -0700 |
---|---|---|
committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-07-07 09:19:13 -0700 |
commit | b0e406ba35be96b525c631f8d1899e5e9eeb0a91 (patch) | |
tree | e94138e921077bd89a6d572c147ae338e812e3bd /tools/TimeFileMaker.py | |
parent | 49a587ec6e6a792bb246dffe16b6fe70bc47897e (diff) |
Output UTF-8 explicitly in timing tools
Diffstat (limited to 'tools/TimeFileMaker.py')
-rw-r--r-- | tools/TimeFileMaker.py | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index ad001012a..b16888c7e 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -1,6 +1,7 @@ from __future__ import with_statement from __future__ import division from __future__ import unicode_literals +from __future__ import print_function import os, sys, re from io import open @@ -206,7 +207,11 @@ def make_table_string(times_dict, def print_or_write_table(table, files): if len(files) == 0 or '-' in files: - print(table) + try: + binary_stdout = sys.stdout.buffer + except AttributeError: + binary_stdout = sys.stdout + print(table.encode("utf-8"), file=binary_stdout) for file_name in files: if file_name != '-': with open(file_name, 'w', encoding="utf-8") as f: |