Hi Bob, thanks for the tips. However ... On 10/30/2012 07:37 PM, Bob Proulx wrote: > Stefano Lattarini wrote: >> Anyway, my /bin/sh is bash ... >> $ ls -l /bin/sh >> lrwxrwxrwx 1 root root 4 Jul 8 2010 /bin/sh -> bash >> I'm on Debian Unstable BTW (sorry for not specifying that earlier). > > Let me say this aside on the issue since there is opportunity for some > confusion. On Debian the default for new installations is that > /bin/sh is a symlink to dash. But existing systems that are upgraded > will not get this change automatically and will remain as a symlink to > bash. It must be specifically selected if desired. > ... I'm not so sure all of scripts on my system are exempt from bashisms; so rather than risking obscure bugs, I'll keep bash as my system shell (for the current system, at least). If it ain't broken, don't fix it ;-)
Best regards, Stefano