we'd better have a Makefile here to prevent the mistake of using
vannilla make instead of gmake.  (But let's leave src/Makefile where
it is, too.)