Re: mantis sets no real domain to filter emails from

2022-09-13 Thread Christian Grothoff
Fixed now. I suspect this happened when Martin last updated Mantis. Thanks for letting us know! -Christian On 9/13/22 21:10, Nikita Ronja Gillmann wrote: Mantis used to set nore...@gnunet.org, now it sets the example.com address for everything. This makes it rather hard to filter when you are

mantis sets no real domain to filter emails from

2022-09-13 Thread Nikita Ronja Gillmann
Mantis used to set nore...@gnunet.org, now it sets the example.com address for everything. This makes it rather hard to filter when you are still on some bug tickets. Can you please fix that to conform to point to gnunet.org? Thanks.