jEdit 5.3pre1 version splash screen always shows; the following options to switch it off do not work:
- uncheck the option 'Show splash screen on startup' in Global Options
- put 'nosplash' file in settings dir
- '-nosplash' argument on command line
tvojeho
Using jEdit version: 5.3pre1
Daily build: 2014-05-25
Java runtime version: 1.7.0_65-b20
OS name: Windows 8.1
OS version: 6.3
OS arch: x86
The bug was introduced in rev http://sourceforge.net/p/jedit/svn/23449 by applying the patch 519:
previously the splashscreen image was shown by the code.
With that patch it is declared in the manifest to be sure to show the splashscreen on top.
It is in fact displayed by the JVM itself. I think that it should be removed and if the splashscreen is not on top that's not a problem, most people don't like this.
Ok to remove that ?
ok to remove that for now.
Note that by calling java -splash:dummy.gif jedit.jar you can disable the splash screen selectively.
One could do the reverse: not having any
SplashScreen-Image: filename.gif in the manifest and selectively adding the -splash:splash.jpg flag to the main jEdit runner (platform dependent: like the .desktop, the .app, etc.).
Fixed in rev 23625