# HG changeset patch # User wenzelm # Date 1224603143 -7200 # Node ID 2cb3369f0634b4127d417dbec1e4c01e0edf6303 # Parent 0b846b3ccc32e9e2d8a8cb6c6fa3d66bda35cddc refined application.args; diff -r 0b846b3ccc32 -r 2cb3369f0634 src/Tools/jEdit/nbproject/project.properties --- a/src/Tools/jEdit/nbproject/project.properties Tue Oct 21 16:21:13 2008 +0200 +++ b/src/Tools/jEdit/nbproject/project.properties Tue Oct 21 17:32:23 2008 +0200 @@ -1,6 +1,6 @@ application.title=Isabelle-jEdit application.vendor=makarius -application.args=-noserver -nobackground -nosettings +application.args=-noserver -nobackground build.classes.dir=${build.dir}/classes build.classes.excludes=**/*.java,**/*.form,**/*.scala # This directory is removed when the project is cleaned: