From 6e2b31ab0ec22c04f8987b4eb54d6ba7bbdee4c4 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Wed, 23 Dec 2020 16:38:31 -0800 Subject: Set the locale in Docker so Python's default output encoding is utf-8 --- doc/README.md | 10 ++++++++++ doc/tools/coqrst/coqdomain.py | 5 +---- 2 files changed, 11 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/README.md b/doc/README.md index 79d1e1b756..440b104c16 100644 --- a/doc/README.md +++ b/doc/README.md @@ -69,6 +69,16 @@ Or if you want to use less disk space: apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \ latexmk fonts-freefont-otf +### Setting the locale for Python + +Make sure that the locale is configured on your platform so that Python encodes +printed messages with utf-8 rather than generating runtime exceptions +for non-ascii characters. The `.UTF-8` in `export LANG=C.UTF-8` sets UTF-8 encoding. +The `C` can be replaced with any supported language code. You can set the default +for a Docker build with `ENV LANG C.UTF-8`. (Python may look at other +environment variables to determine the locale; see the +[Python documentation](https://docs.python.org/3/library/locale.html#locale.getdefaultlocale)). + Compilation ----------- 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 -- cgit v1.2.3