|
From: mike d. <md...@st...> - 2000-01-20 02:41:38
|
On Wed, 19 Jan 2000, Kevin A. Burton wrote:
> mode.xml.filenameGlob=*.{xml,sgml,sgm,dtd,rdf,rss,xsd}
>
> But jEdit still didn't pick these up. Are the file extension hard coded
> and ignoring the Glob?
the globs are only loaded from the global and plugin properties. the user
properties do not affect them. you must edit org/gjt/sp/jedit/jedit.props
and update the JAR file instead.
-md
|