diff -r f7f0d516df0c -r 26cd26aaf108 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue May 18 21:09:51 2021 +0200
+++ b/src/Doc/System/Sessions.thy	Tue May 18 22:02:21 2021 +0200
@@ -238,6 +238,12 @@
     is occasionally useful to control the global visibility of commands via
     session options (e.g.\ in \<^verbatim>\<open>ROOT\<close>).
 
+    \<^item> @{system_option_def "document_preprocessor"} specifies the name of an
+    executable that is run within the document output directory, after
+    preparing the document sources and before the actual build process. This
+    allows to apply adhoc patches, without requiring a separate \<^verbatim>\<open>build\<close>
+    script.
+
     \<^item> @{system_option_def "threads"} determines the number of worker threads
     for parallel checking of theories and proofs. The default \<open>0\<close> means that a
     sensible maximum value is determined by the underlying hardware. For