summaryrefslogtreecommitdiff
path: root/debian/rules
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-16 22:00:15 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-16 22:00:15 +0000
commit97cc3f9bb7f50a9d38494b3a4c5fa78384f1cf79 (patch)
tree68a19d4a04a8095ace784ce8f0cbc69d21417df4 /debian/rules
parent87d0789ec9533e2efc5513d5a50d3a4e3d641d82 (diff)
Added a manpage for coqide.
Diffstat (limited to 'debian/rules')
-rwxr-xr-xdebian/rules3
1 files changed, 3 insertions, 0 deletions
diff --git a/debian/rules b/debian/rules
index 19396fad..beb3d42c 100755
--- a/debian/rules
+++ b/debian/rules
@@ -71,6 +71,9 @@ install: build
dh_install --sourcedir=$(COQPREF)
cp debian/coq/usr/share/man/man1/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1
+ cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.1
+ cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.byte.1
+ cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.opt.1
binary-indep: build install