NEWS
changeset 17869 585c1f08499e
parent 17865 5b0c3dcfbad2
child 17878 5b9efe4d6b47
--- a/NEWS	Sat Oct 15 00:09:20 2005 +0200
+++ b/NEWS	Sat Oct 15 00:14:30 2005 +0200
@@ -11,8 +11,8 @@
 
 *** Document preparation ***
 
-* Added antiquotations @{ML_type text} and @{ML_struct} which check
-the given source text as ML type/structure, printing verbatim.
+* Added antiquotations @{ML_type text} and @{ML_struct text} which
+check the given source text as ML type/structure, printing verbatim.
 
 
 *** Pure ***