| Tue, 01 Nov 2016 15:12:45 +0100 | wenzelm | ignore interrupts from underlying process, e.g. due to out-of-memory situation in ML_Process (see also build.scala); | changeset | files |
| Tue, 01 Nov 2016 15:00:27 +0100 | wenzelm | proper remote repository source; | changeset | files |
| Tue, 01 Nov 2016 14:59:50 +0100 | wenzelm | clarified setup_repository: even more uniform pull vs. clone (see also e84cba30d7ff); | changeset | files |