summaryrefslogtreecommitdiff
path: root/debian/coqide.dirs
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/coqide.dirs
parent87d0789ec9533e2efc5513d5a50d3a4e3d641d82 (diff)
Added a manpage for coqide.
Diffstat (limited to 'debian/coqide.dirs')
-rw-r--r--debian/coqide.dirs1
1 files changed, 1 insertions, 0 deletions
diff --git a/debian/coqide.dirs b/debian/coqide.dirs
index f783eb3a..1add6cd0 100644
--- a/debian/coqide.dirs
+++ b/debian/coqide.dirs
@@ -1,2 +1,3 @@
usr/share/doc/coqide
usr/share/applnk/Development
+usr/share/man/man1