# HG changeset patch
# User wenzelm
# Date 1393584494 -3600
# Node ID a1a8378bda422b2b2ccdf4564f59d095134aae40
# Parent  985bd3a325ab7effef2f43f0d7c16936bad8cd32
tuned comment;

diff -r 985bd3a325ab -r a1a8378bda42 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Feb 28 11:46:54 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Feb 28 11:48:14 2014 +0100
@@ -219,7 +219,7 @@
 
 (** main state -- document structure and execution process **)
 
-type blob_digest = (string * string option) Exn.result;  (* file name, raw digest*)
+type blob_digest = (string * string option) Exn.result;  (* file node name, raw digest*)
 
 type execution =
  {version_id: Document_ID.version,  (*static version id*)