src/Tools/jEdit/etc/settings
changeset 70220 089753519be0
parent 66906 03a96b8c7c06
child 71790 97fc4f657bda
--- a/src/Tools/jEdit/etc/settings	Tue Apr 30 17:03:32 2019 +0100
+++ b/src/Tools/jEdit/etc/settings	Tue Apr 30 20:54:07 2019 +0200
@@ -3,7 +3,7 @@
 JEDIT_HOME="$COMPONENT"
 JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
 
-JEDIT_OPTIONS="-reuseview -nobackground -log=9"
+JEDIT_OPTIONS="-reuseview -nobackground -nosplash -log=9"
 
 JEDIT_JAVA_OPTIONS="-Xms512m -Xmx2560m -Xss8m"
 JEDIT_JAVA_SYSTEM_OPTIONS="-Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"