Use sys.getdefaultencoding() instead of sys.stdout.encoding

doc/mk_params_doc.py

@@ -37,7 +37,7 @@ def help(ous):
     out = subprocess.Popen([z3_exe, "-pm"],stdout=subprocess.PIPE).communicate()[0]
     modules = ["global"]
     if out != None:
-        out = out.decode(sys.stdout.encoding)
+        out = out.decode(sys.getdefaultencoding())
         module_re = re.compile(r"\[module\] (.*)\,")
         lines = out.split("\n")
         for line in lines:
@@ -48,7 +48,7 @@ def help(ous):
             out = subprocess.Popen([z3_exe, "-pmmd:%s" % module],stdout=subprocess.PIPE).communicate()[0]
             if out == None:
                 continue
-            out = out.decode(sys.stdout.encoding)
+            out = out.decode(sys.getdefaultencoding())
             out = out.replace("\r","")
             ous.write(out)
 

doc/mk_tactic_doc.py

@@ -28,7 +28,7 @@ def extract_params(ous, tac):
     out = subprocess.Popen([z3_exe, f"-tacticsmd:{tac}"], stdout=subprocess.PIPE).communicate()[0]
     if not out:
         return
-    out = out.decode(sys.stdout.encoding)
+    out = out.decode(sys.getdefaultencoding())
     if is_ws(out):
         return
     ous.write("### Parameters\n\n")

scripts/mk_util.py

@@ -122,7 +122,7 @@ def getenv(name, default):
 def check_output(cmd):
     out = subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]
     if out != None:
-        enc = sys.stdout.encoding
+        enc = sys.getdefaultencoding()
         if enc != None: return out.decode(enc).rstrip('\r\n')
         else: return out.rstrip('\r\n')
     else:

scripts/update_api.py

@@ -1836,14 +1836,14 @@ def _to_pystr(s):
 else:
   def _str_to_bytes(s):
     if isinstance(s, str):
-        enc = sys.stdout.encoding
+        enc = sys.getdefaultencoding()
         return s.encode(enc if enc != None else 'latin-1')
     else:
         return s
 
   def _to_pystr(s):
      if s != None:
-        enc = sys.stdout.encoding
+        enc = sys.getdefaultencoding()
         return s.decode(enc if enc != None else 'latin-1')
      else:
         return ""