# HG changeset patch # User wenzelm # Date 1558174110 -7200 # Node ID 110df6f913766353ab90a96cc55150e23770179e # Parent a3862cf94e73b5dc2c39dd60ff59b3932ded5463 tuned; diff -r a3862cf94e73 -r 110df6f91376 NEWS --- a/NEWS Tue May 14 10:28:07 2019 +0200 +++ b/NEWS Sat May 18 12:08:30 2019 +0200 @@ -125,7 +125,7 @@ presentation context or to emit markup to the PIDE document. Some predefined markers are taken from the Dublin Core Metadata Initiative, e.g. \<^marker>\contributor arg\ or \<^marker>\license arg\ and produce PIDE markup that -can retrieved from the document database. +can be retrieved from the document database. * Old-style command tags %name are re-interpreted as markers with proof-scope \<^marker>\tag (proof) name\ and produce LaTeX environments as