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