aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorHugo Herbelin2020-07-14 18:23:31 +0200
committerHugo Herbelin2020-11-22 13:28:40 +0100
commit87c46c50506089ba16bdd7afd7e795ee21033319 (patch)
tree83097b8fb1664f404296e4b4c09ebefe620bd50a /dev
parentdf8b5c7d83ad6e88af34d29bcc32c85bd42c2712 (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 'dev')
0 files changed, 0 insertions, 0 deletions