diff -r 756434c77d21 -r 7857817403e4 etc/options
--- a/etc/options	Wed May 16 21:06:28 2018 +0200
+++ b/etc/options	Wed May 16 21:07:12 2018 +0200
@@ -189,8 +189,8 @@
 option editor_syslog_limit : int = 100
   -- "maximum amount of buffered syslog messages"
 
-public option editor_document_output : bool = false
-  -- "dynamic document output while editing"
+public option editor_presentation : bool = false
+  -- "dynamic presentation while editing"
 
 
 section "Miscellaneous Tools"