Re: build from CVS

[Stefan Monnier]

>     Assuming that make expands $$ to it's PID, does it ?
> 
> I think make starts a shell to run the command, so $$ will
> be the PID of the shell.  So I expect it would not work.
> Have you ever seen it ever work?

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.

With some shells you might be able to use `$$PPID'.


        Stefan