users_guide: Set flags list file encoding
authorBen Gamari <ben@smart-cactus.org>
Thu, 7 Nov 2019 03:04:25 +0000 (22:04 -0500)
committerMarge Bot <ben+marge-bot@smart-cactus.org>
Fri, 8 Nov 2019 02:25:36 +0000 (21:25 -0500)
Otherwise this fails on Windows.

docs/users_guide/flags.py

index 90d6921..dcc6743 100644 (file)
@@ -602,7 +602,7 @@ def process_print_nodes(app, doctree, fromdocname):
         node.generate_output(app, fromdocname)
 
     # Write out file listing all documented flags
-    with open(os.path.join(app.outdir, 'ghc-flags.txt'), 'w') as f:
+    with open(os.path.join(app.outdir, 'ghc-flags.txt'), 'w', encoding='utf-8') as f:
         flag_names = \
             {name
              for flag in app.env.all_flags