On Sat, 23 Jul 2022, 15:46 Waldek Hebisch, <[email protected]> wrote:
> On Sat, Jul 23, 2022 at 09:17:06AM +0800, Qian Yun wrote: > > There were several times that GitHub does not display email replies > > from Waldek. This is already causing headaches for me and I think > > this situation is bad for the collaboration of the FriCAS project. > > > > First, I understand that, for privacy reasons or other reasons, > > an email based workflow can be preferred over a web based one. > > > > I can think of 2 solutions right now: > > > > 1. It seems that Waldek is using one email account for googlegroups > > and another email account for GitHub replies. I guess you are > > managing the 2 email accounts in a single email client locally. > > If so, I wonder if it is possible/convenient to send the reply > > to googlegroups/GitHub issues through 2 email accounts simultaneously. > > ATM the accounts are on two different machines. As popular > saying goes doing what you propose is SMOP (small matter of > programming), but I would prefer to spent my programming time > on FriCAS and not on mail software. And also see below... > > > 2. Setup some GitHub Actions script to forward every GitHub issue > > comments to fricas-devel. Then when the issue is resolved, we can > > sync the status back to GitHub. > > Primary reason that I directed Github messages to separate > address is that Github can be quite spammy, there is a lot > of trivial messsages. Duplicating messages would add to > the problem. > > I must admit that my prefered information flow would be > as follows: > - issues in Github issue tracker. But if there is need > for discussion it should be in mailing list > - in general discussions (including proposed changes) > in mailing list > - changes as patches (diff files) > > I understand that third point (patches) is disliked by > other people here, but up to now I did not figure out > how to merge Github pull request using _only_ git commands. > what exactly is not working here for you? GitHub PRs git branches are just, well, git branches, so producing and pushing a merged branch is possible with git commands only. Marking the PR as resolved, on the other hand, seems tricky, if at all possible. There are command line tools for this, so a browser is not needed, ( e.g. tig, see https://jonas.github.io/tig/ ) but one would need to authenticate to GitHub once. Since I unable to use git commands ATM handling merging > pull requests is extremally inconvenient for me. > > -- > Waldek Hebisch > > -- > You received this message because you are subscribed to the Google Groups > "FriCAS - computer algebra system" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/fricas-devel/20220723134615.GB30366%40fricas.math.uni.wroc.pl > . > -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/CAAWYfq20a_vkC7-O402krS52DwL9McT78ruOW%2BZAiTJy1vswKA%40mail.gmail.com.
