etc/options
changeset 68197 7857817403e4
parent 68184 6c693b2700b3
child 68221 dbef88c2b6c5
--- 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"