diff options
| author | Théo Zimmermann | 2020-11-14 16:01:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-18 16:24:30 +0100 |
| commit | 3b479357d8c5c1a655b2b8257f14a8cafe7621fc (patch) | |
| tree | 72b1d9d04a9adfc81739b2e70f81e3f0b95abd7f /doc/tools | |
| parent | 0af10d808de19f1f052fab3c757f4049fa0c3ec8 (diff) | |
Run doc_grammar for #13312.
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 1 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 033ece04de..b5d57f92e9 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -764,6 +764,7 @@ attribute: [ attr_value: [ | "=" string +| "=" IDENT | "(" attribute_list ")" | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index dfd3a18908..c9d70a88fc 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -383,6 +383,7 @@ attribute: [ attr_value: [ | "=" string +| "=" ident | "(" LIST0 attribute SEP "," ")" ] |