Commit 1badfd5d85cedfe06a2d8262f0ae91b121e86fa5

Bruno Haible 2019-01-27T22:57:45

Accommodate a shell that is not in /bin/sh.