1 files changed, 7 insertions, 0 deletions
diff --git a/debian/patches/00list b/debian/patches/00list
new file mode 100644
index 00000000..333bbd2f
--- /dev/null
+++ b/debian/patches/00list
@@ -0,0 +1,7 @@
+camlp5
+coqdoc_stdlib
+browser
+makefile
+no-complexity-test
+configure
+cmxa-install