# 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