Makefile not quite right

[Henry Cejtin]

Well,  I'm  confused.   Yes,  I  am  talking about the Makefile in src/mlton.
Despite the setting of PATH, after making the mlton there, typing
    make -n
does indeed try to execute the mlton in  that  directory.   The  same  occurs
without the `-n'.  Note, this is in the case where there is nothing to do.  I
deduce that the PATH setting is NOT effecting the things inside of
    $(shell ...)
things since these should be the only mlton calls running.  It  looks  pretty
insane to me,

As  to  the name, I don't care what the name is, I just don't think it should
be `mlton'.  `mlton1' and `mltonc' both seem a  bit  random.   I  would  pick
`grind' or `mlton.grind' or something, but it really doesn't matter.