On Thu, Apr 23, 2009 at 10:04:15PM +0100, Matthias Scheler wrote: > But it is something we could consider on platforms which > use /bin/bash as /bin/sh. If you switch any platform to pdksh simply for performance reasons, please state so clearly in bootstrap, so that it can be revisited later. Joerg