diff options
| -rw-r--r-- | docs/users_guide/flags.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/users_guide/flags.py b/docs/users_guide/flags.py index 90d6921827..dcc6743d18 100644 --- a/docs/users_guide/flags.py +++ b/docs/users_guide/flags.py @@ -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 |