# 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>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> 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>\<open>tag (proof) name\<close> and produce LaTeX environments as