aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
authorThéo Zimmermann2020-11-14 16:01:00 +0100
committerEmilio Jesus Gallego Arias2020-11-18 16:24:30 +0100
commit3b479357d8c5c1a655b2b8257f14a8cafe7621fc (patch)
tree72b1d9d04a9adfc81739b2e70f81e3f0b95abd7f /doc/sphinx
parent0af10d808de19f1f052fab3c757f4049fa0c3ec8 (diff)
Run doc_grammar for #13312.
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/language/core/basic.rst1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index af5c47dba8..ea29da6dd4 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -369,6 +369,7 @@ this attribute`.
attributes ::= {* #[ {*, @attribute } ] } {* @legacy_attr }
attribute ::= @ident {? @attr_value }
attr_value ::= = @string
+ | = @ident
| ( {*, @attribute } )
legacy_attr ::= {| Local | Global }
| {| Polymorphic | Monomorphic }