src/Tools/jEdit/dist-template/interface
Sat, 20 Dec 2008 00:14:25 +0100 wenzelm more robust handling of FILES with spaces, using bash array variables;
Fri, 19 Dec 2008 23:56:58 +0100 wenzelm disabled tracing;
Fri, 19 Dec 2008 23:54:24 +0100 wenzelm proper spelling of JEDIT_JAVA_OPTIONS;
Tue, 21 Oct 2008 23:52:17 +0200 wenzelm added jvmpath conversion for Cygwin;
Tue, 21 Oct 2008 22:27:53 +0200 wenzelm explicit home path for default file -- more robust;
Tue, 21 Oct 2008 22:00:11 +0200 wenzelm disabled tracing;
Tue, 21 Oct 2008 21:48:16 +0200 wenzelm Isabelle/jEdit interface wrapper.
less more (0) tip