# HG changeset patch
# User wenzelm
# Date 1754856446 -7200
# Node ID 4629fcbf53e23c72a551acdcb9d959777a257ba9
# Parent  839d86abfe86ed4a3a4992f2f20a023a3829351c
tuned;

diff -r 839d86abfe86 -r 4629fcbf53e2 etc/options
--- a/etc/options	Sun Aug 10 22:06:24 2025 +0200
+++ b/etc/options	Sun Aug 10 22:07:26 2025 +0200
@@ -162,7 +162,7 @@
   -- "ML profiling (possible values: time, time_thread, allocations)"
 
 option profiling_dir : string = "" for content
-  -- "output directory for \"isabelle profiling\" tool"
+  -- "auxiliary directory for \"isabelle profiling\" tool"
 
 option system_log : string = "" (standard "-") for build
   -- "output for system messages (log file or \"-\" for console progress)"