<div dir="auto"><div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Vaclav Petras <<a href="mailto:wenzeslaus@gmail.com">wenzeslaus@gmail.com</a>> schrieb am Fr., 1. Sep. 2023, 16:45:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>I just realized this would also be a good match for the grass-announce mailing list. To cross-post or not to cross-post?<br></div></div></blockquote></div></div><div dir="auto"><br></div><div dir="auto">Yes, cross-post.</div><div dir="auto"><br></div><div dir="auto">Markus</div><div dir="auto"><br></div></div>