+# I think some of the GNU documentation suggests that we shouldn't
+# rely on shell functions. However, the Bash manual seems to say that
+# they're in POSIX 1003.2, and since the build farm relies on them
+# they're probably working on most machines we really care about.