summaryrefslogtreecommitdiff
path: root/debian/coqide.dirs
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 17:37:10 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 19:32:36 +0100
commit4ac272f0121ba8f3ab48a18c8225b44b03bba4f7 (patch)
tree86068ebd7d6a132ece9727ef3dd4e0b1c3f5927e /debian/coqide.dirs
parentf231ae59d9189649cb69262376b2f2dab4b543a2 (diff)
Miscellaneous updates
Diffstat (limited to 'debian/coqide.dirs')
-rw-r--r--debian/coqide.dirs4
1 files changed, 0 insertions, 4 deletions
diff --git a/debian/coqide.dirs b/debian/coqide.dirs
index bf32ae9c..c1da623a 100644
--- a/debian/coqide.dirs
+++ b/debian/coqide.dirs
@@ -1,5 +1 @@
-usr/lib/coq/ide
-usr/share/doc/coqide
-usr/share/applications
-usr/share/man/man1
usr/share/pixmaps