# HG changeset patch
# User wenzelm
# Date 1283539178 -7200
# Node ID 9bac2f4cfd6e5b6ba65a64e015cd5ea925c16d82
# Parent  01214c68f8bccea14fa8d52eb74bb22a6a178a5d
tuned comment;

diff -r 01214c68f8bc -r 9bac2f4cfd6e src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Fri Sep 03 18:03:48 2010 +0200
+++ b/src/Pure/General/print_mode.ML	Fri Sep 03 20:39:38 2010 +0200
@@ -3,6 +3,8 @@
 
 Generic print mode as thread-local value derived from global template;
 provides implicit configuration for various output mechanisms.
+
+The special print mode "input" is never enabled for output.
 *)
 
 signature BASIC_PRINT_MODE =