diff options
| author | Pierre Roux | 2020-09-04 15:09:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:20:28 +0200 |
| commit | 754e138e1e1c86dcd5e9d07084a5d33a5056ce9d (patch) | |
| tree | 55772785eadac1c653f587f9d0338e5ba9c2dfdc /doc/tools/docgram/common.edit_mlg | |
| parent | 46b9480a717d5ca78e354fa843f39eed87cb7b15 (diff) | |
[refman] Rename numeral to number
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? *) |