aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-03-02 22:55:24 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-03-02 22:55:24 +0000
commitd0ef012305eb65b83f125d3316373a0698e18293 (patch)
treee6fe98f37fe7682d02927954001dd9ea8ebbd0c6 /Makefile
parentf08f8b6bb2dc70c0737058097846eb6e46f36301 (diff)
Fix info install
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 369ce49c..e7153b60 100644
--- a/Makefile
+++ b/Makefile
@@ -196,8 +196,8 @@ install-doc: doc.info
cp -pf doc/proofgeneral.1 ${MANDIR}
mkdir -p ${INFODIR}
cp -pf doc/*.info ${INFODIR}
- /sbin/install-info /usr/share/info/ProofGeneral.info.* ${INFODIR}/dir
- /sbin/install-info /usr/share/info/PG-adapting.info.* ${INFODIR}/dir
+ /sbin/install-info ${INFODIR}/ProofGeneral.info* ${INFODIR}/dir
+ /sbin/install-info ${INFODIR}/PG-adapting.info* ${INFODIR}/dir
doc.%:
(cd doc; make $*)