On 1/9/23 11:35, Niko Tyni wrote:
Hi, this is about a difference in bash vs. dash as /bin/sh.
Thank you for the prompt and detailed reply. I agree that fixing Dash seems like the correct solution. I will investigate the alternatives you suggest.
David
