| Mon, 24 Oct 2016 12:16:12 +0200 | wenzelm | discontinued unused / untested distinction of separate PIDE modules; | changeset | files |
| Mon, 24 Oct 2016 12:01:36 +0200 | wenzelm | proper Admin tool; | changeset | files |
| Mon, 24 Oct 2016 11:48:32 +0200 | wenzelm | tuned message; | changeset | files |
| Mon, 24 Oct 2016 11:42:39 +0200 | wenzelm | updated for release; | changeset | files |
| Mon, 24 Oct 2016 11:10:17 +0200 | wenzelm | updated to jedit_build-20161024: Code2HTML 0.7, Navigator 2.7; | changeset | files |
| Mon, 24 Oct 2016 14:32:07 +0100 | paulson | Merge | changeset | files |
| Mon, 24 Oct 2016 14:31:05 +0100 | paulson | "subgoal" examples | changeset | files |