Re: [Bug-dejagnu] [patch] dejagnu 1.4.3: DESTDIR for dejagnu.h

[Rob Savoye]

On Tue, Oct 29, 2002 at 01:45:18PM +0100, Maciej W. Rozycki wrote:

>  There is a small problem when installing dejagnu.h.  It doesn't use
> DESTDIR possibly leading to installation failures.  Here is a patch to fix
> it.  Please apply. 

  Thanks for the patch, I got two identical versions of this while I was
gone on a work trip, so if you don't mind, I used both your names in the
ChangeLog entry. Thanks for sending a patch with your bug report! 

        - rob -