summaryrefslogtreecommitdiff
path: root/debian/coqide.install
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-07-28 15:54:36 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-07-28 15:54:36 +0200
commit4cc16f522c193923b93d38d637a6dcae1e1a96b7 (patch)
tree421626e304aed18c77d07ddbe027be3c4d8c087d /debian/coqide.install
parentdb0c2d0f86e7fb2153be13431641a2fad0babf90 (diff)
ide/utf8.v is not there anymore (moved to theories)
Diffstat (limited to 'debian/coqide.install')
-rw-r--r--debian/coqide.install1
1 files changed, 0 insertions, 1 deletions
diff --git a/debian/coqide.install b/debian/coqide.install
index f214e01c..238c4fdd 100644
--- a/debian/coqide.install
+++ b/debian/coqide.install
@@ -1,4 +1,3 @@
usr/bin/coqide*
usr/lib/coq/ide/coq.png
-usr/lib/coq/ide/utf8.vo
usr/lib/coq/ide/.coqide-gtk2rc