From: Stephane Glondu <steph@glondu.net>
Date: Fri, 18 Mar 2011 15:38:36 +0000 (+0100)
Subject: Add debian/source/local-options
X-Git-Tag: archive/raspbian/4.08.1-4+rpi1~3^2~323
X-Git-Url: https://dgit.raspbian.org/?a=commitdiff_plain;h=1e0d9bb1d7499ef9e78fb03314c4bbd108cb128c;p=ocaml.git

Add debian/source/local-options
---

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 00000000..845ca067
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+.pc
diff --git a/debian/gbp.conf b/debian/gbp.conf
index ef8fd01d..d84e16cf 100644
--- a/debian/gbp.conf
+++ b/debian/gbp.conf
@@ -1,5 +1,4 @@
 [DEFAULT]
 pristine-tar = True
-cleaner = debuild clean && dh_quilt_unpatch && dh_clean
 upstream-branch = 312/upstream
 debian-branch = 312/master
diff --git a/debian/source/local-options b/debian/source/local-options
new file mode 100644
index 00000000..c4cf4805
--- /dev/null
+++ b/debian/source/local-options
@@ -0,0 +1,2 @@
+abort-on-upstream-changes
+unapply-patches