From: Stephane Glondu <steph@glondu.net>
Date: Wed, 24 Jul 2019 07:37:47 +0000 (+0200)
Subject: Remove debian/source/local-options
X-Git-Tag: archive/raspbian/4.08.1-4+rpi1~2^2~17^2~31
X-Git-Url: https://dgit.raspbian.org/?a=commitdiff_plain;h=b8f150719e65db5efc78afb271f01cb1e02e5a85;p=ocaml.git

Remove debian/source/local-options
---

diff --git a/debian/source/local-options b/debian/source/local-options
deleted file mode 100644
index c4cf4805..00000000
--- a/debian/source/local-options
+++ /dev/null
@@ -1,2 +0,0 @@
-abort-on-upstream-changes
-unapply-patches