diff -r 77b51733ffdf -r 3e8395f9093a etc/options
--- a/etc/options	Wed Nov 11 21:09:56 2020 +0100
+++ b/etc/options	Wed Nov 11 22:20:57 2020 +0100
@@ -8,7 +8,9 @@
 option document : string = ""
   -- "build document in given format: pdf, dvi, false"
 option document_output : string = ""
-  -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
+  -- "document output directory"
+option document_output_sources : bool = true
+  -- "copy generated sources into document output directory"
 option document_variants : string = "document"
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""