aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-07-08 12:36:45 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-07-08 12:36:45 -0400
commita44b4be1bf8b96e941216cd10cfb5981a825c3fa (patch)
tree033fbe56cd25893bf3b87399dc27e2dcf79dcc1c /tools
parent39ba36bfa1ee2aa951dbad9f518bde81e45f3e9d (diff)
parentb0e406ba35be96b525c631f8d1899e5e9eeb0a91 (diff)
Merge PR #8015: 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 872a73282..8b6822a4e 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -90,9 +90,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: