From 647f158228b54574c675079e1a010fa2e1c8698d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 3 Apr 2013 12:16:01 +0200 Subject: [PATCH] adding patch --- .../0001-set-DESTDIR-to-debian-tmp.patch | 26 +++++++++++++++++++ debian/patches/series | 1 + 2 files changed, 27 insertions(+) create mode 100644 debian/patches/0001-set-DESTDIR-to-debian-tmp.patch create mode 100644 debian/patches/series 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 index 0000000..a812e6c --- /dev/null +++ b/debian/patches/0001-set-DESTDIR-to-debian-tmp.patch @@ -0,0 +1,26 @@ +From: Enrico Tassi +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 index 0000000..7e66bf5 --- /dev/null +++ b/debian/patches/series @@ -0,0 +1 @@ +0001-set-DESTDIR-to-debian-tmp.patch -- 2.39.2