« Previous | Next » 

Revision 38d9d95d

ID38d9d95d23f65e0b8bd17b514f1bc2571d5f96de
Parent 7c18ef8e
Child 9dda7cb1

Added by Michael Hanselmann over 15 years ago

Use DESTDIR when creating additional directories.

Reviewed-by: iustinp

Files

  • added
  • modified
  • copied
  • renamed
  • deleted

View differences