etc/options

--- a/etc/options	Mon May 14 22:01:00 2018 +0200
+++ b/etc/options	Mon May 14 22:22:47 2018 +0200
@@ -189,6 +189,9 @@
 option editor_syslog_limit : int = 100
   -- "maximum amount of buffered syslog messages"
 
+public option editor_document_output : bool = false
+  -- "dynamic document output while editing"
+
 
 section "Miscellaneous Tools"