debian/patches/0001-set-DESTDIR-to-debian-tmp.patch

   1 From: Enrico Tassi <gares@fettunta.org>
   2 Date: Wed, 3 Apr 2013 12:11:01 +0200
   3 Subject: set DESTDIR to debian/tmp
   4
   5 ---
   6  plugin/Makefile |    4 ++--
   7  1 file changed, 2 insertions(+), 2 deletions(-)
   8
   9 diff --git a/plugin/Makefile b/plugin/Makefile
  10 index 5bf2892..534aea4 100644
  11 --- a/plugin/Makefile
  12 +++ b/plugin/Makefile
  13 @@ -31,10 +31,10 @@ PLUGIN_CMO = eset emap completeMap multiset misc arithSig arith             \
  14         compute_simple compute_simple_stack_size cerco cost
  15
  16  # PLUGIN_HAS_MLI := yes
  17 -
  18 +DESTDIR=../debian/tmp/
  19  # include Makefile.plugin
  20  include $(FRAMAC_SHARE)/Makefile.dynamic
  21
  22  distclean: clean
  23
  24 -.PHONY = distclean
  25 \ No newline at end of file
  26 +.PHONY = distclean