diff options
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 1 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 17fc220f6c..3a0c3a8bc7 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -2557,6 +2557,7 @@ deprecated_number_modifier: [ number_mapping: [ | reference "=>" reference +| "[" reference "]" "=>" reference ] number_via: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 3d1041e592..13d8979208 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1282,7 +1282,7 @@ number_modifier: [ ] number_via: [ -| "via" qualid "mapping" "[" LIST1 ( qualid "=>" qualid ) SEP "," "]" +| "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" ] hints_path: [ |