[pretty-print py]Don't print sys.stdout;better utf

This should fix #9705

I'm kind-of cargo-cult coding here, from things like
https://docs.python.org/3/library/sys.html#sys.displayhook and
https://github.com/coq/coq/issues/9705#issuecomment-471996313, but
hopefully this fixes the issue without breaking anything.  (I am really
a novice when it comes to the str/bytes distinction in python3.)

1 files changed, 4 insertions, 5 deletions

diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py
index 854dd25b75..0c5fdb50ac 100644
--- a/tools/TimeFileMaker.py
+++ b/tools/TimeFileMaker.py
@@ -209,11 +209,10 @@ def make_table_string(times_dict,
 
 def print_or_write_table(table, files):
     if len(files) == 0 or '-' in files:
-        try:
-            binary_stdout = sys.stdout.buffer
-        except AttributeError:
-            binary_stdout = sys.stdout
-        print(table.encode("utf-8"), file=binary_stdout)
+        if hasattr(sys.stdout, 'buffer'):
+            sys.stdout.buffer.write(table.encode("utf-8"))
+        else:
+            sys.stdout.write(table)
     for file_name in files:
         if file_name != '-':
             with open(file_name, 'w', encoding="utf-8") as f: