NEWS
changeset 42358 b47d41d9f4b5
parent 42290 b1f544c84040
child 42360 da8817d01e7c
     1.1 --- a/NEWS	Sat Apr 16 12:46:18 2011 +0200
     1.2 +++ b/NEWS	Sat Apr 16 13:48:45 2011 +0200
     1.3 @@ -37,6 +37,13 @@
     1.4  Note that automated detection from the file-system or search path has
     1.5  been discontinued.  INCOMPATIBILITY.
     1.6  
     1.7 +* Name space: proper configuration options "long_names",
     1.8 +"short_names", "unique_names" instead of former unsynchronized
     1.9 +references.  Minor INCOMPATIBILITY, need to declare options in context
    1.10 +like this:
    1.11 +
    1.12 +  declare [[unique_names = false]]
    1.13 +
    1.14  
    1.15  *** HOL ***
    1.16