fix: fix-comments.py uses wrong encoding on Windows (leanprover-com…

…munity#2761) Another issue is that it writes the output with CRLF newlines. I tried to fix it but failed. Co-authored-by: Johan Commelin <[email protected]>
WenrongZou · Mar 10, 2023 · b9eddd1 · b9eddd1
1 parent 756f130
commit b9eddd1
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/scripts/fix-comments.py b/scripts/fix-comments.py
@@ -41,7 +41,7 @@
 
 name_map = dict()
 for f in align_files.stdout.splitlines():
-    with open(os.path.join(root_dir, f)) as fh:
+    with open(os.path.join(root_dir, f), encoding="utf-8") as fh:
         contents = fh.read()
         for p in contents.split(sep='\n#align')[1:]:
             n3, n4, *_ = p.split(maxsplit=2)
@@ -84,7 +84,7 @@ def finish_comment():
         in_line_comment = False
         comment_so_far = None
 
-with open(leanfile) as F:
+with open(leanfile, encoding="utf-8") as F:
     while 1:
         char = F.read(1)
         if not char: