From 22aa11b21202a44c35da70970da6b34479c4a815 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 16 Dec 2014 16:28:34 +0100
Subject: In CHANGES, alerting about stronger check on notation level
 modifiers.

---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGES b/CHANGES
index 1eca0a5185..5f23119d91 100644
--- a/CHANGES
+++ b/CHANGES
@@ -256,6 +256,8 @@ Notations
   or error when this notation is used.
 - More systematic insertion of spaces as a default for printing
   notations ("format" still available to override the default).
+- In notations, a level modifier referring to a non-existent variable is
+  now considered an error rather than silently ignored.
 
 Tools
 
-- 
cgit v1.2.3