[MLton] mlnlffigen is awesome (was: bootstrap problem)

[Henry Cejtin]

I would say that using ~/.mlton/mlb-path-map by default is fine.  I would
vote for allowing multiple -mlb-path-map arguments, allowing later ones to
override earlier ones.  The only question is: do we disable the use of
~/.mlton/mlb-path-map by the presence of any -mlb-path-map args?  If so,
then you might need to do the weird
	-mlb-path-map /dev/null
to indicate no variables at all.