From c20769ad4851ee7fa99605fed6b89964e147cddc Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 17 Apr 2021 13:07:41 +0200
Subject: Remove superfluous sort.

Removing it makes no difference to the order of glossary entries,
which is determined by the "for ... sorted" statement above.
---
 doc/tools/coqrst/coqdomain.py | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index edb8db1e94..1ab4fe8f81 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -1180,8 +1180,7 @@ class StdGlossaryIndex(Index):
             if type == 'term':
                 entries = content[itemname[0].lower()]
                 entries.append([itemname, 0, docname, anchor, '', '', ''])
-        content = sorted(content.items())
-        return content, False
+        return content.items(), False
 
 def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
     """A grammar production not included in a ``prodn`` directive.
-- 
cgit v1.2.3