[jedit] 04/09: Remove source/options file because xz is the default now.

[Markus Koschany]

This is an automated email from the git hooks/post-receive script.

apo pushed a commit to branch master
in repository jedit.

commit b36b9293fd0edf1945ba4d1953e29ec0332c2aa0
Author: Markus Koschany <apo at debian.org>
Date:   Wed Nov 29 22:49:49 2017 +0100

    Remove source/options file because xz is the default now.
---
 debian/source/options | 1 -
 1 file changed, 1 deletion(-)

diff --git a/debian/source/options b/debian/source/options
deleted file mode 100644
index b7bc1f2..0000000
--- a/debian/source/options
+++ /dev/null
@@ -1 +0,0 @@
-compression = "xz"

-- 
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-java/jedit.git