bug fix : doc's Makefile now handle DESTDIR

diff --git a/doc/Makefile.in b/doc/Makefile.in
index 93ead7239067252356765e2df74fe65c28a7caa1..ab71e024a54e4edb9f48097112efda2930a26002 100644 (file)
--- a/doc/Makefile.in
+++ b/doc/Makefile.in
@@ -4,7 +4,7 @@
 
 # @configure_input@
 
-# $Id: Makefile.in,v 1.10 2002-07-19 19:43:25 thib Exp $
+# $Id: Makefile.in,v 1.11 2002-08-22 21:35:56 thib Exp $
 
 # The following should not be edited manually (use configure options)
 # If you must do it, BEWARE : some of the following is also defined
@@ -15,8 +15,8 @@
 SRCDIR         = @srcdir@
 
 prefix         = @prefix@
-DESTMAN                = @mandir@
-DESTDOC                = @DOCDIR@
+DESTMAN                = $(DESTDIR)@mandir@
+DESTDOC                = $(DESTDIR)@DOCDIR@
 
 INSTALL                = @INSTALL@
 JADE           = @JADE@