-
Committer:
Jelmer Vernooij
-
Date:
2019-01-13 19:54:14 UTC
-
Revision ID:
jelmer@jelmer.uk-20190113195414-516gle4f4drn882u
Change priority extra to priority optional.
Fixes lintian: priority-extra-is-replaced-by-priority-optional
See https://lintian.debian.org/tags/priority-extra-is-replaced-by-priority-optional.html for more details.