# HG changeset patch
# User wenzelm
# Date 1742746075 -3600
# Node ID 94fd80f0107d211fa5ce804973fc6d8505b8c1a1
# Parent  0811cfce1f5b9ded998f1a40fbf13068391fef91
remove junk (amending 0811cfce1f5b);

diff -r 0811cfce1f5b -r 94fd80f0107d src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sun Mar 23 15:12:20 2025 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Mar 23 17:07:55 2025 +0100
@@ -239,7 +239,7 @@
     -f           fresh build
     -i NAME      include session in name-space of theories
     -j OPTION    add jEdit runtime option
-                 (default -reuseview -nobackground -nosplash -log=9)
+                 (default $JEDIT_OPTIONS)
     -l NAME      logic session name
     -m MODE      add print mode for output
     -n           no build of session image on startup