On Sat, Jul 23, 2022 at 04:02:42PM +0200, Dima Pasechnik wrote:
> On Sat, 23 Jul 2022, 15:46 Waldek Hebisch, <[email protected]>
> wrote:
>
> > 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.
First problem is to have good address for this branch. IIRC
I found info how to fetch this branch, but I was not able to
do what I needed apparently due to permission problems.
Part of problem seem to be that Github associates permissions
with address that one uses and that they disabled password
authentication. That breaks old instructions. And I did
not find up-to date instructions (actually since old
instructions that I found did not work I did not copy them
so I have no instruction new or old).
--
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/20220725175007.GA24189%40fricas.math.uni.wroc.pl.
