aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-07-07 09:19:13 -0700
committerGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-07-07 09:19:13 -0700
commitb0e406ba35be96b525c631f8d1899e5e9eeb0a91 (patch)
treee94138e921077bd89a6d572c147ae338e812e3bd /tools
parent49a587ec6e6a792bb246dffe16b6fe70bc47897e (diff)
Output UTF-8 explicitly in timing tools
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in6
-rw-r--r--tools/TimeFileMaker.py7
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: