# HG changeset patch
# User wenzelm
# Date 1224514923 -7200
# Node ID be2e9e6726af183c9eb8f0939ba66411def81299
# Parent  2c0d7132361904c19249f453954397b567b2971c
added application.args (Why does it end up in pricate properties?);

diff -r 2c0d71323619 -r be2e9e6726af src/Tools/jEdit/nbproject/project.properties
--- a/src/Tools/jEdit/nbproject/project.properties	Mon Oct 20 16:46:28 2008 +0200
+++ b/src/Tools/jEdit/nbproject/project.properties	Mon Oct 20 17:02:03 2008 +0200
@@ -1,5 +1,6 @@
 application.title=Isabelle-jEdit
 application.vendor=makarius
+application.args=-noserver -nobackground -nosettings
 build.classes.dir=${build.dir}/classes
 build.classes.excludes=**/*.java,**/*.form,**/*.scala
 # This directory is removed when the project is cleaned: