Note: I didn't test this change.
Attempting to fix an error I got locally:
File "C:\Users\Floris\AppData\Local\Programs\Python\Python311\Lib\site-packages\leanblueprint\Packages\blueprint.py", line 236, in make_lean_data
lean_decls_path.write_text("\n".join(document.userdata.get("lean_decls", [])))
File "C:\Users\Floris\AppData\Local\Programs\Python\Python311\Lib\pathlib.py", line 1079, in write_text
return f.write(data)
^^^^^^^^^^^^^
File "C:\Users\Floris\AppData\Local\Programs\Python\Python311\Lib\encodings\cp1252.py", line 19, in encode
return codecs.charmap_encode(input,self.errors,encoding_table)[0]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
UnicodeEncodeError: 'charmap' codec can't encode character '\u0398' in position 259: character maps to <undefined>
plasTeX version 3.1
Command 'plastex -c plastex.cfg web.tex' returned non-zero exit status 1.
Note: I didn't test this change. Attempting to fix an error I got locally: