# HG changeset patch
# User wenzelm
# Date 1407575881 -7200
# Node ID 28e17057b5456df290537b52fa76876595d3470d
# Parent  be1bcec136630d0f6dc8481e4abf92366ee707ff
tuned comments;

diff -r be1bcec13663 -r 28e17057b545 src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Fri Aug 08 22:05:02 2014 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Sat Aug 09 11:18:01 2014 +0200
@@ -2,7 +2,7 @@
     Author:     Makarius
 
 One-shot query operations via asynchronous print functions and temporary
-document overlay.
+document overlays.
 *)
 
 signature QUERY_OPERATION =