| Fri, 05 Oct 2018 23:49:12 +0200 | wenzelm | discontinue java.ext.dirs for jdk-11 -- in contrast to 982f0bf34804 for jdk-8; | changeset | files |
| Fri, 05 Oct 2018 17:49:10 +0200 | nipkow | more [simp] | changeset | files |
| Thu, 04 Oct 2018 16:40:03 +0200 | wenzelm | avoid TCP_NODELAY (in contrast to 18c621069bf8): might cause problems with some versions of Ubuntu 18.04; | changeset | files |
| Thu, 04 Oct 2018 15:25:58 +0100 | paulson | merged | changeset | files |