[m-rev.] packaging diff: Fix package priority

[Paul Bone]

Fix package priority

The "extra" package priority is now known as "optional"

debian/control:
    As above.
---
 debian/control | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/debian/control b/debian/control
index 07ed225..4c2af42 100644
--- a/debian/control
+++ b/debian/control
@@ -1,6 +1,6 @@
 Source: mercury
 Section: devel
-Priority: extra
+Priority: optional
 Maintainer: Paul Bone <paul at bone.id.au>
 Build-Depends: debhelper (>=9), autoconf, automake, flex, bison,
   libreadline-dev, texinfo, texi2html, libhwloc-dev, pkg-config
-- 
2.17.1