| Sun, 15 Mar 2020 11:38:36 +0100 | wenzelm | more robust connection via proxy_host; | changeset | files |
| Sat, 14 Mar 2020 21:58:29 +0100 | wenzelm | more robust: proper transfer if Context.eq_thy_id; | changeset | files |
| Sat, 14 Mar 2020 20:36:16 +0100 | wenzelm | merged | changeset | files |
| Sat, 14 Mar 2020 14:23:52 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 14 Mar 2020 13:49:52 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 14 Mar 2020 13:44:52 +0100 | wenzelm | more robust hg_url; | changeset | files |
| Fri, 13 Mar 2020 23:50:18 +0100 | wenzelm | proper usage (amending 8c7706b053c7); | changeset | files |