diff options
| author | Hugo Herbelin | 2020-07-14 18:23:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-22 13:28:40 +0100 |
| commit | 87c46c50506089ba16bdd7afd7e795ee21033319 (patch) | |
| tree | 83097b8fb1664f404296e4b4c09ebefe620bd50a /plugins | |
| parent | df8b5c7d83ad6e88af34d29bcc32c85bd42c2712 (diff) | |
Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".
For constr, this means clarifying that "ident" is deprecated and to be
replaced by "name". Here, some cleaning shall have to be done at the
end of deprecation phase, when "ident" will take its literal meaning.
For custom notations, this is about documenting the effect of "ident"
and "global" which was yet undocumented.
Note that we anticipate an example in constr working with the literal
meaning of "ident" (temporarily silencing the warning).
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions
