From b4e88c15da749b3edbd56cb70bf280a8e7bbfc3c Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Mon, 16 Jul 2018 14:04:29 -0700
Subject: Add test for repeated section with same name

---
 doc/sphinx/language/gallina-extensions.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index d9b2490452..394b928ada 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -781,7 +781,8 @@ Section :ref:`gallina-definitions`).
 
 .. cmd:: Section @ident
 
-   This command is used to open a section named `ident`.
+   This command is used to open a section named :token:`ident`.
+   Section names do not need to be unique.
 
 
 .. cmd:: End @ident
-- 
cgit v1.2.3