diff options
| author | Jim Fehrle | 2020-12-23 16:38:31 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2020-12-26 15:47:48 -0800 |
| commit | 6e2b31ab0ec22c04f8987b4eb54d6ba7bbdee4c4 (patch) | |
| tree | 74e47a1864c4eab8d6c3d77e52e12975e32fee56 /doc/tools | |
| parent | 687fff698db75d54ef0a8b156b85a4dc027edc62 (diff) | |
Set the locale in Docker so Python's default output encoding is utf-8
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 8f642df8fd..35243b5d7d 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -220,10 +220,7 @@ class CoqObject(ObjectDescription): # todo: then maybe the above "if" is not needed names_in_subdomain = self.subdomain_data() if name in names_in_subdomain: - try: - print("Duplicate", self.subdomain, "name: ", name) - except UnicodeEncodeError: # in CI - print("*** UnicodeEncodeError") + print("Duplicate", self.subdomain, "name: ", name) # self._warn_if_duplicate_name(names_in_subdomain, name, signode) return targetid |