diff -r 161e84e6b40a -r 015282fb3e31 etc/options
--- a/etc/options	Mon Nov 08 12:45:35 2021 +0100
+++ b/etc/options	Mon Nov 08 13:51:24 2021 +0100
@@ -9,6 +9,8 @@
   -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")"
 option document_output : string = ""
   -- "document output directory"
+option document_echo : bool = false
+  -- "inform about document file names during session presentation"
 option document_variants : string = "document"
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""