Not all /bin/sh like echo -e.

Paul Dekkers made me aware of the fact that "echo -e" doesn't work with /bin/sh on his system. I think he's running some Linux and I bet they've replaced /bin/sh with dash or something. (I wish they would stop replacing /bin/sh.)

The scripts in tools could use printf(1) instead, if we think that's present on all modern platforms. Do we think so?