aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-03-02 22:48:16 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-03-02 22:48:16 +0000
commitf08f8b6bb2dc70c0737058097846eb6e46f36301 (patch)
tree367c8e8bd1db2a69436232bd5d0a7b88f3593e39 /Makefile
parentcb1a561b535e9aeae10a385509fa1166b8cc53f7 (diff)
Oops. Fix DEST_PREFIX mistake in paths.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile10
1 files changed, 5 insertions, 5 deletions
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