diff options
| author | Pierre Roux | 2020-09-03 13:23:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:19 +0100 |
| commit | 0520decfdc94d52a2f8658b9cf6a730e6d333f8f (patch) | |
| tree | 56130ed8dafe578760221bbc6e7d7d835ac4791c /doc/tools/docgram/orderedGrammar | |
| parent | 9082af80f5bb70ff2b75117f9e5cc3165b1c8b42 (diff) | |
[numeral notation] Handle implicit arguments
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 2 |
1 files changed, 1 insertions, 1 deletions
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: [ |