src/Tools/jEdit/lib/Tools/jedit_client
Sat, 02 Jan 2016 17:38:00 +0100 wenzelm proper platform_path for Windows;
Wed, 30 Sep 2015 21:32:44 +0200 wenzelm renamed jvmpath to platform_path;
Mon, 14 Sep 2015 16:06:32 +0200 wenzelm added isabelle jedit_client;
less more (0) tip