# HG changeset patch
# User wenzelm
# Date 1754991125 -7200
# Node ID 947d10dbe353dee7559f7a077978044303380fc7
# Parent  4a77ce6d4e07056a24e5fd705bcdb554d44d9582
no special tag for transient option;

diff -r 4a77ce6d4e07 -r 947d10dbe353 etc/options
--- a/etc/options	Tue Aug 12 11:19:08 2025 +0200
+++ b/etc/options	Tue Aug 12 11:32:05 2025 +0200
@@ -161,7 +161,7 @@
 option profiling : string = "" (standard "time") for build
   -- "ML profiling (possible values: time, time_thread, allocations)"
 
-option profiling_dir : string = "" for content
+option profiling_dir : string = ""
   -- "auxiliary directory for \"isabelle profiling\" tool"
 
 option system_log : string = "" (standard "-") for build