From 19d5ebc6477686d2c57d44a08c5d200cc74db931 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 24 May 2020 15:41:06 +0200
Subject: Fix #12280: do not use xindy to avoid build failures on some
 machines.

---
 doc/README.md      | 3 +--
 doc/sphinx/conf.py | 3 +++
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/README.md b/doc/README.md
index 8e1bc85c49..e3ab5ae4d2 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -58,7 +58,6 @@ additional tools are required:
   - makeindex
   - xelatex
   - latexmk
-  - xindy
 
 All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu,
 install them with:
@@ -68,7 +67,7 @@ install them with:
 Or if you want to use less disk space:
 
     apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
-                latexmk xindy fonts-freefont-otf
+                latexmk fonts-freefont-otf
 
 Compilation
 -----------
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index fabf7a519f..9a6fd2272b 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -356,6 +356,9 @@ latex_elements = {
 
 latex_engine = "xelatex"
 
+# Cf. https://github.com/sphinx-doc/sphinx/issues/7015
+latex_use_xindy = False
+
 ########
 # done #
 ########
-- 
cgit v1.2.3