Sorry, little omission: the first example under section 3 is not with
bash, it was done with dash.