diff -r 6560324b1e4d -r 6c693b2700b3 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"