| Thu, 25 Feb 2016 18:05:04 +0100 | wenzelm | avoid global state change; | changeset | files |
| Thu, 25 Feb 2016 17:49:04 +0100 | wenzelm | more robust treatment of shell functions: dynamic_env recreates lost definitions on demand, e.g. after going through aggressive versions of /bin/sh -> dash; | changeset | files |
| Thu, 25 Feb 2016 16:53:34 +0000 | paulson | Merge | changeset | files |