diff options
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index ff40555696..fbf83760ad 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -770,7 +770,7 @@ int: [ | OPT "-" natural ] -numeral: [ +number: [ | OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat ) | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat ) ] @@ -795,7 +795,7 @@ ident: [ ] NUMBER: [ -| numeral +| number ] (* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *) |