aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/fullGrammar
diff options
context:
space:
mode:
authorPierre Roux2020-09-03 13:23:00 +0200
committerPierre Roux2020-11-05 00:20:19 +0100
commit0520decfdc94d52a2f8658b9cf6a730e6d333f8f (patch)
tree56130ed8dafe578760221bbc6e7d7d835ac4791c /doc/tools/docgram/fullGrammar
parent9082af80f5bb70ff2b75117f9e5cc3165b1c8b42 (diff)
[numeral notation] Handle implicit arguments
Diffstat (limited to 'doc/tools/docgram/fullGrammar')
-rw-r--r--doc/tools/docgram/fullGrammar1
1 files changed, 1 insertions, 0 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: [