[MLton] [PATCH] Man-page updates

[Matthew Fluet]

On Sat, 23 Feb 2008, Jesper Louis Andersen wrote:
> A patch is attached to this file proposing a man-page update.
>
> I don't think we are distributing ps.gz files anymore, but rather pdf files.
> Case in point:
>
> ogre% grep -r pdf Makefile
>                bin/make-pdf-guide; \
>        if [ -r "$(TDOC)/guide/mlton-guide.pdf" ]; then                 \
>                mv "$(TDOC)/guide/mlton-guide.pdf" "$(TDOC)/";          \
>        $(CP) $(LEX)/$(LEX).pdf $(TDOC)
>        $(CP) $(YACC)/$(YACC).pdf $(TDOC)
>
> Reflect this in the man-page. The hinted location is the default location on
> Linux. I'll take the change in the FreeBSD port with a patch to the man-page
> as it tends to be a lot easier than having to run a M4/CPP preprocessor step
> on the man-pages.
>
> I'll commit if you agree.

Looks fine.