Menu

#3876 Splash screen in v5.3 can't be turned off

closed-fixed
nobody
None
5
2014-07-28
2014-07-25
tvojeho
No

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

Discussion

  • Matthieu Casanova

    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 ?

     
  • Eric Le Lay

    Eric Le Lay - 2014-07-26

    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.).

     
  • Matthieu Casanova

    Fixed in rev 23625

     
  • Matthieu Casanova

     
  • Matthieu Casanova

    • status: open --> closed-fixed
     

Log in to post a comment.