This directory is for the MINITS sources.  Nothing else should be
kept here, there are other directories for other things.