I have added "disputed" label there as I disagree with the metadata of the PR in question, not the least because it uses my idea without giving a due credit.
Given that PR author blocks me on GitHub, I take this as a further personal attack, which should stop at once. First a developer blocks someone, then the developer steals their ideas, is this a kind of behaviour we should tolerate? Dima On 13 August 2024 20:53:11 BST, 'Martin R' via sage-devel <sage-devel@googlegroups.com> wrote: >I must say that I find this response intolerable. > >I cannot quit, because I have duties, but I am really pissed off. > >Martin >On Tuesday 13 August 2024 at 21:41:54 UTC+2 Matthias Koeppe wrote: > >> I marked Martin's message as off-topic because PR discussions are not a >> place for discussions about procedure. >> >> On Tuesday, August 13, 2024 at 2:04:13 AM UTC-7 Martin R wrote: >> >>> I asked a question at https://github.com/sagemath/sage/pull/38219 which >>> was promptly labelled off topic, so I suppose I should ask it here: >>> >>> The preceding message on the pull request was: >>> >>> I have removed the improper use of the "disputed" label. >>> >>> My question (and comment) was: >>> >>> Why is the use "improper"? Apart from that, it seems to me that >>> removing the disputed label should only be possible with consensus. >>> >>> My new question is: >>> >>> Why is my question labelled "off topic"? Where should labelling >>> issues be discussed. >>> >>> I am rather puzzled and quite a bit worried. I find it hard to deal with >>> this kind of culture of conversation. >>> >>> Martin >>> >> > >-- >You received this message because you are subscribed to the Google Groups >"sage-devel" group. >To unsubscribe from this group and stop receiving emails from it, send an >email to sage-devel+unsubscr...@googlegroups.com. >To view this discussion on the web visit >https://groups.google.com/d/msgid/sage-devel/0cb70224-8c09-4320-8db6-b0defbbd2cb9n%40googlegroups.com. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/D6C11238-512A-4661-8E9C-DF85FC85C727%40gmail.com.
