On 7/23/22 21:46, Waldek Hebisch 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...
Just saying objectively (no judging), your dislike to use GitHub
web interface is in someway, is similar to Tim Daly's insistence
on the usage of literature programming. (Not saying whether it is
good or bad, just 99% people don't do things like that.) This choice
is easier for you, but it might not be the best for the community and
thus not best for the future of FriCAS.
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.
Since I unable to use git commands ATM handling merging
pull requests is extremally inconvenient for me.
Although I do not use it myself, you can operate GitHub in command line:
https://cli.github.com/
Also, in the future, I'll try to post patches to maillist then.
- Qian
--
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/ed74a275-82fa-607c-6fdc-46216e8d42ff%40gmail.com.
