summaryrefslogtreecommitdiff
path: root/debian/coqide.install
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-01-31 22:22:12 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 01:17:59 +0100
commitae6bfcaa882c9841c5d91ff40dca8b77260202b6 (patch)
tree989c52acc833c761745e0112c2c0f7fd4a8608d7 /debian/coqide.install
parent02896b211aaec508c4e4591e7e228f752b368fd7 (diff)
Simplify handling of dispatch to binary packages
Diffstat (limited to 'debian/coqide.install')
-rw-r--r--debian/coqide.install1
1 files changed, 1 insertions, 0 deletions
diff --git a/debian/coqide.install b/debian/coqide.install
index dd6bf116..52eec4db 100644
--- a/debian/coqide.install
+++ b/debian/coqide.install
@@ -1,4 +1,5 @@
usr/bin/coqide*
usr/lib/coq/ide/coq.png
usr/lib/coq/ide/.coqide-gtk2rc
+usr/lib/coq/ide/FAQ
usr/share/man/man1/coqide*