| Wed, 09 Jan 2013 21:59:53 +0100 | wenzelm | refrain from writing to JEDIT_SETTINGS in BUILD_ONLY mode -- relevant for makedist; | changeset | files |
| Wed, 09 Jan 2013 21:24:16 +0100 | wenzelm | renamed tool; | changeset | files |
| Wed, 09 Jan 2013 21:21:41 +0100 | wenzelm | create required PREFS_DIR; | changeset | files |
| Wed, 09 Jan 2013 18:35:51 +0100 | wenzelm | eliminated choosefrom -- power-users may edit global defaults within script; | changeset | files |
| Wed, 09 Jan 2013 18:32:26 +0100 | wenzelm | tuned; | changeset | files |
| Wed, 09 Jan 2013 18:12:21 +0100 | wenzelm | updated makebundles as Admin isabelle tool; | changeset | files |
| Wed, 09 Jan 2013 17:04:59 +0100 | wenzelm | tuned; | changeset | files |