Output UTF-8 explicitly in timing tools

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: