diff options
Diffstat (limited to 'doc/changelog/03-notations/10180-deprecate-notations.rst')
| -rw-r--r-- | doc/changelog/03-notations/10180-deprecate-notations.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst index 01f2e893ed..bce5db5865 100644 --- a/doc/changelog/03-notations/10180-deprecate-notations.rst +++ b/doc/changelog/03-notations/10180-deprecate-notations.rst @@ -2,5 +2,5 @@ attribute. The former `compat` annotation for notations is deprecated, and its semantics changed. It is now made equivalent to using a `deprecated` attribute, and is no longer connected with the `-compat` - command-line flag. + command-line flag (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). |