387388389390391392393394395396397
// splash DocSplashViewer splash = new DocSplashViewer("splash.gif", "DocSearcher " + I18n.getString("ds.version") + " " + I18n.getString("ds.isloading")); if (! hasCommands) { splash.display(); } // gets OS type env.setOSType(Utils.getOSType());