adding patch

diff --git a/debian/patches/0001-set-DESTDIR-to-debian-tmp.patch b/debian/patches/0001-set-DESTDIR-to-debian-tmp.patch
new file mode 100644 (file)
index 0000000..a812e6c
--- /dev/null
+++ b/debian/patches/0001-set-DESTDIR-to-debian-tmp.patch
@@ -0,0 +1,26 @@
+From: Enrico Tassi <gares@fettunta.org>
+Date: Wed, 3 Apr 2013 12:11:01 +0200
+Subject: set DESTDIR to debian/tmp
+
+---
+ plugin/Makefile |    4 ++--
+ 1 file changed, 2 insertions(+), 2 deletions(-)
+
+diff --git a/plugin/Makefile b/plugin/Makefile
+index 5bf2892..1800191 100644
+--- a/plugin/Makefile
++++ b/plugin/Makefile
+@@ -31,10 +31,10 @@ PLUGIN_CMO = eset emap completeMap multiset misc arithSig arith            \
+       compute_simple compute_simple_stack_size cerco cost
+ 
+ # PLUGIN_HAS_MLI := yes
+-
++DESTDIR=debian/tmp/
+ # include Makefile.plugin
+ include $(FRAMAC_SHARE)/Makefile.dynamic
+ 
+ distclean: clean
+ 
+-.PHONY = distclean
+\ No newline at end of file
++.PHONY = distclean

diff --git a/debian/patches/series b/debian/patches/series
new file mode 100644 (file)
index 0000000..7e66bf5
--- /dev/null
+++ b/debian/patches/series
@@ -0,0 +1 @@
+0001-set-DESTDIR-to-debian-tmp.patch