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/tools/coqrst/coqdomain.py | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'doc/tools')

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