From f08f8b6bb2dc70c0737058097846eb6e46f36301 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 2 Mar 2004 22:48:16 +0000
Subject: Oops.  Fix DEST_PREFIX mistake in paths.

---
 Makefile | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index c1d7e33c..369ce49c 100644
--- a/Makefile
+++ b/Makefile
@@ -134,11 +134,11 @@ endif
 ELISP=${PREFIX}/${ELISPP}
 DEST_ELISP=${DEST_PREFIX}/${ELISPP}
 
-BINDIR=${DEST_PREFIX}/bin
-DESKTOP=${DEST_PREFIX}/share
-DOCDIR=${DEST_PREFIX}/share/doc/ProofGeneral
-MANDIR=${DEST_PREFIX}/share/man/man1
-INFODIR=${DEST_PREFIX}/share/info/
+BINDIR=${PREFIX}/bin
+DESKTOP=${PREFIX}/share
+DOCDIR=${PREFIX}/share/doc/ProofGeneral
+MANDIR=${PREFIX}/share/man/man1
+INFODIR=${PREFIX}/share/info/
 
 install: install-desktop install-elisp install-bin install-init
 
-- 
cgit v1.2.3