summaryrefslogtreecommitdiff
path: root/debian/patches/00list
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
commit783b26ca58daa06d66776ddf1b50a20268e0c4b0 (patch)
tree52419c783a4072ebbd789e47ccecd15ecd3418e9 /debian/patches/00list
parentff1dde8f1585c92dd69a9a41ad709f15ef8936da (diff)
New upstream release.debian/8.1.pl2+dfsg-1
Diffstat (limited to 'debian/patches/00list')
-rw-r--r--debian/patches/00list1
1 files changed, 0 insertions, 1 deletions
diff --git a/debian/patches/00list b/debian/patches/00list
index 333bbd2f..bbb91a76 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1,4 +1,3 @@
-camlp5
coqdoc_stdlib
browser
makefile