From: Stephane Glondu <steph@glondu.net>
Date: Tue, 6 Aug 2019 07:31:06 +0000 (+0200)
Subject: Remove debian/source/local-options
X-Git-Tag: archive/raspbian/4.08.1-4+rpi1~3^2~13
X-Git-Url: https://dgit.raspbian.org/?a=commitdiff_plain;h=e34b649daf684bf2ed1f05d00a9e72125c4eb889;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