tuned spelling;
authorwenzelm
Mon, 07 Aug 2017 14:06:24 +0200
changeset 66369 d003b44674c1
parent 66368 26735fab7a8f
child 66370 de9c6560c221
tuned spelling;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Aug 07 11:34:32 2017 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Aug 07 14:06:24 2017 +0200
@@ -58,7 +58,7 @@
  {header: node_header,  (*master directory, theory header, errors*)
   keywords: Keyword.keywords option,  (*outer syntax keywords*)
   perspective: perspective,  (*command perspective*)
-  entries: Command.exec option Entries.T,  (*command entries with excecutions*)
+  entries: Command.exec option Entries.T,  (*command entries with executions*)
   result: Command.eval option}  (*result of last execution*)
 and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
 with