# HG changeset patch # User immler@in.tum.de # Date 1225724591 -3600 # Node ID 74ddfd2cf5a5575dcd8209311f8388c3957f410b # Parent 1c919f65c2967fe9f4c145df5e6f8036c16a5fd9 using 'dist' directory for jEdit-settings => find Isabelle-plugin directly diff -r 1c919f65c296 -r 74ddfd2cf5a5 src/Tools/jEdit/nbproject/project.properties --- a/src/Tools/jEdit/nbproject/project.properties Sun Nov 02 16:28:37 2008 +0100 +++ b/src/Tools/jEdit/nbproject/project.properties Mon Nov 03 16:03:11 2008 +0100 @@ -16,7 +16,12 @@ ${run.test.classpath} # This directory is removed when the project is cleaned: dist.dir=dist -dist.jar=${dist.dir}/Isabelle-jEdit.jar +# dist can be used as jEdits settings-directory; +# jEdit searches for plugins in the 'jars' subdirectory +# must include something like this to private.properties: +# application.args=-noserver -nobackground -settings=/absolute/path/to/project/dist +# +dist.jar=${dist.dir}/jars/Isabelle-jEdit.jar dist.javadoc.dir=${dist.dir}/javadoc excludes= file.reference.isabelle-jedit-src=src