On 02/11/2018 06:12 PM, Jason Duerstock wrote: > This has been pushed upstream as https://github.com/seqan/seqan/issues/2281
Be careful, "pushed" is misleading here. It's not been pushed yet as in it has been merged. You merely filed an issue unless I missed the commit. Adrian -- .''`. John Paul Adrian Glaubitz : :' : Debian Developer - [email protected] `. `' Freie Universitaet Berlin - [email protected] `- GPG: 62FF 8A75 84E0 2956 9546 0006 7426 3B37 F5B5 F913

