diff -r f7f0d516df0c -r 26cd26aaf108 etc/options
--- a/etc/options	Tue May 18 21:09:51 2021 +0200
+++ b/etc/options	Tue May 18 22:02:21 2021 +0200
@@ -13,6 +13,8 @@
   -- "alternative document variants (separated by colons)"
 option document_tags : string = ""
   -- "default command tags (separated by commas)"
+option document_preprocessor : string = ""
+  -- "document preprocessor: executable relative to document output directory"
 option document_build : string = "lualatex"
   -- "document build engine (e.g. lualatex, pdflatex, build)"
 option document_logo : string = ""