Re: [ jEdit-devel ] How to distribute additional files for a plugin?

[Slava P. <sl...@je...>]

Hi,

Right now the only way to do this is for your plugin's start() method
to check if the files exist, and if not, copy the default set from
your plugin's JAR (using getResourceAsStream()).

Slava

On Tue, Nov 13, 2001 at 08:23:52PM +0100, Klaus Hartlage wrote:
> I would like to copy additional files for a plugin in a directory:
> <users.home>/.jedit/<plugin-name>/<jedit-mode-name>/script.bsh
> 
> How does the plugin manager download/install such files?
> Is there a method or special beanshell script in the plugin interface, 
> which is called if the plugin manager installs the plugin?
> 
> -- 
> Klaus Hartlage
> Math java project:  http://www.hartmath.org
> Riding the Java wave: http://www.jsurfer.org
> 
> 
> -- 
> -----------------------------------------------
> jEdit Developers' List
> jEd...@li...
> https://lists.sourceforge.net/lists/listinfo/jedit-devel