From 73a2675e35b25c65582c02516943b0dd010016dd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 19 Oct 2020 10:37:09 +0200 Subject: Adding change log for #12984. Co-authored-by: Ralf Jung --- .../12984-master+import-notation-make-active-again.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst (limited to 'doc') diff --git a/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst new file mode 100644 index 0000000000..d472e6fdf0 --- /dev/null +++ b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst @@ -0,0 +1,12 @@ +- **Changed:** + Redeclaring a notation reactivates also its printing rule; in + particular a second :cmd:`Import` of the same module reactivates the + printing rules declared in this module. In theory, this leads to + changes of behavior for printing. However, this is mitigated in + general by the adoption in `#12986 + `_ of a priority given to + notations which match a larger part of the term to print + (`#12984 `_, + fixes `#7443 `_ + and `#10824 `_, + by Hugo Herbelin). -- cgit v1.2.3