diff -r 488a48453d74 -r 9e5f8f6e58a0 etc/options
--- a/etc/options	Thu Mar 16 13:18:25 2023 +0100
+++ b/etc/options	Thu Mar 16 15:16:17 2023 +0100
@@ -174,6 +174,9 @@
 
 section "Build Process"
 
+option build_thorough : bool = false
+  -- "observe dependencies on options with tag 'content' or 'document'"
+
 option build_hostname : string = ""
   -- "alternative hostname for build process (default $ISABELLE_HOSTNAME)"