fix patch

diff --git a/debian/patches/0001-set-DESTDIR-to-debian-tmp.patch b/debian/patches/0001-set-DESTDIR-to-debian-tmp.patch
index a812e6c5adf1a5cf5ec76d94a078150b2cb64c17..b044f1c5af471977d1e2d8170a836c628e496732 100644 (file)
--- a/debian/patches/0001-set-DESTDIR-to-debian-tmp.patch
+++ b/debian/patches/0001-set-DESTDIR-to-debian-tmp.patch
@@ -7,7 +7,7 @@ Subject: set DESTDIR to debian/tmp
  1 file changed, 2 insertions(+), 2 deletions(-)
 
 diff --git a/plugin/Makefile b/plugin/Makefile
-index 5bf2892..1800191 100644
+index 5bf2892..534aea4 100644
 --- a/plugin/Makefile
 +++ b/plugin/Makefile
 @@ -31,10 +31,10 @@ PLUGIN_CMO = eset emap completeMap multiset misc arithSig arith            \
@@ -15,7 +15,7 @@ index 5bf2892..1800191 100644
  
  # PLUGIN_HAS_MLI := yes
 -
-+DESTDIR=debian/tmp/
++DESTDIR=../debian/tmp/
  # include Makefile.plugin
  include $(FRAMAC_SHARE)/Makefile.dynamic