# HG changeset patch
# User wenzelm
# Date 1754910050 -7200
# Node ID 50673a1d90f295027e737ba42cc10487a819d55c
# Parent  71ffc2c2234823f0dfea8cb2a7349998de67678d
update documentation, following 71ffc2c22348;

diff -r 71ffc2c22348 -r 50673a1d90f2 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Aug 11 12:34:58 2025 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Aug 11 13:00:50 2025 +0200
@@ -1214,6 +1214,7 @@
     -H REGEX     filter messages by matching against head
     -M REGEX     filter messages by matching against body
     -O           output messages
+    -U           output Unicode symbols
     -d DIR       include session directory
     -f FILE      include addition session files
     -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
@@ -1245,8 +1246,8 @@
   spot using @{tool build}. Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> work as in @{tool
   build}.
 
-  Option \<^verbatim>\<open>-O\<close> enables output of prover messages. Options \<^verbatim>\<open>-H\<close>, \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-m\<close>
-  work as in @{tool build_log}.
+  Option \<^verbatim>\<open>-O\<close> enables output of prover messages. Options \<^verbatim>\<open>-H\<close>, \<^verbatim>\<open>-M\<close>, \<^verbatim>\<open>-U\<close>,
+  \<^verbatim>\<open>-m\<close> work as in @{tool build_log}.
 \<close>