From b0e406ba35be96b525c631f8d1899e5e9eeb0a91 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Sat, 7 Jul 2018 09:19:13 -0700 Subject: Output UTF-8 explicitly in timing tools --- tools/CoqMakefile.in | 6 +++--- tools/TimeFileMaker.py | 7 ++++++- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 2ebe4aba7..7aa2d0a5a 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -91,9 +91,9 @@ COQDOC ?= "$(COQBIN)coqdoc" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts -COQMAKE_ONE_TIME_FILE ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-one-time-file.py" -COQMAKE_BOTH_TIME_FILES ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-both-time-files.py" -COQMAKE_BOTH_SINGLE_TIMING_FILES ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-both-single-timing-files.py" +COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" BEFORE ?= AFTER ?= 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: -- cgit v1.2.3