NEWS
changeset 39689 78b185bf7660
parent 39644 ad436fa9fc5b
child 39754 150f831ce4a3
     1.1 --- a/NEWS	Fri Sep 24 15:56:29 2010 +0200
     1.2 +++ b/NEWS	Fri Sep 24 16:17:59 2010 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  * Discontinued ancient 'constdefs' command.  INCOMPATIBILITY, use
     1.5  'definition' instead.
     1.6  
     1.7 -* Document antiquotations 'class' and 'type' for printing classes
     1.8 +* Document antiquotations @{class} and @{type} for printing classes
     1.9  and type constructors.
    1.10  
    1.11