summaryrefslogtreecommitdiff
path: root/debian/coqide.docs
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.docs
parentf231ae59d9189649cb69262376b2f2dab4b543a2 (diff)
Miscellaneous updates
Diffstat (limited to 'debian/coqide.docs')
-rw-r--r--debian/coqide.docs1
1 files changed, 0 insertions, 1 deletions
diff --git a/debian/coqide.docs b/debian/coqide.docs
deleted file mode 100644
index 6fcc323e..00000000
--- a/debian/coqide.docs
+++ /dev/null
@@ -1 +0,0 @@
-ide/FAQ