NEWS
changeset 70281 110df6f91376
parent 70260 22cfcfcadd8b
child 70294 742f8e703780
child 70297 67edf0234417
     1.1 --- a/NEWS	Tue May 14 10:28:07 2019 +0200
     1.2 +++ b/NEWS	Sat May 18 12:08:30 2019 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4  presentation context or to emit markup to the PIDE document. Some
     1.5  predefined markers are taken from the Dublin Core Metadata Initiative,
     1.6  e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
     1.7 -can retrieved from the document database.
     1.8 +can be retrieved from the document database.
     1.9  
    1.10  * Old-style command tags %name are re-interpreted as markers with
    1.11  proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as