From 4595cc3b66adfcdd0c070106207f62835d261fb2 Mon Sep 17 00:00:00 2001
From: Lukas Puehringer <lukas.puehringer@nyu.edu>
Date: Wed, 7 Aug 2019 16:04:54 +0200
Subject: [PATCH] Remove unnecessary debian source/options file

Signed-off-by: Lukas Puehringer <lukas.puehringer@nyu.edu>
---
 debian/source/options | 11 -----------
 1 file changed, 11 deletions(-)
 delete mode 100644 debian/source/options

diff --git a/debian/source/options b/debian/source/options
deleted file mode 100644
index b99e0e3c..00000000
--- a/debian/source/options
+++ /dev/null
@@ -1,11 +0,0 @@
-# Default ignore patterns contains *.o and *.a. So we need to define our own
-# patterns to get them included.
---tar-ignore=.*.sw?
---tar-ignore=*/*~
---tar-ignore=,,*
---tar-ignore=.[#~]*
---tar-ignore=.deps
---tar-ignore=.git
---tar-ignore=.gitattributes
---tar-ignore=.gitignore
---tar-ignore=.gitmodules