Tue, 14 Aug 2012 13:01:09 +0200 | wenzelm | clarified format of etc/options: only declarations, not re-definitions; | changeset | files |
Tue, 14 Aug 2012 12:26:02 +0200 | wenzelm | check_errors for cumulative session content; | changeset | files |
Tue, 14 Aug 2012 12:21:32 +0200 | wenzelm | even more defensive path expansion (see also 8d381fdef898); | changeset | files |
Tue, 14 Aug 2012 11:43:08 +0200 | wenzelm | support for 'typ' with explicit sort constraint; | changeset | files |
Tue, 14 Aug 2012 11:37:58 +0200 | wenzelm | added jedit option -d; | changeset | files |
Tue, 14 Aug 2012 10:44:03 +0200 | wenzelm | always retain doc-src (as regular component); | changeset | files |
Mon, 13 Aug 2012 20:31:24 +0200 | wenzelm | merged | changeset | files |