Re: build from CVS

[Richard Stallman]

    Actually, `$$' is turned into `$' by make (since $ is used by make for
    variable interpolation, `$$' is provided as a way to protect a $ from
    expansion).  So `$$$$' would get the shell's process id.

I stand corrected, but this doesn't affect the point.  The shell's
process id is not useful anyway--killing the shell is easy with `exit
1', but that won't tell `make -k' to stop.