On Tue, Jul 26, 2022 at 09:02:02AM +0200, Dima Pasechnik wrote:
> On Tue, Jul 26, 2022 at 1:42 AM Waldek Hebisch
> <[email protected]> wrote:
> >
> > On Tue, Jul 26, 2022 at 12:54:33AM +0200, Dima Pasechnik wrote:
> > > On Mon, Jul 25, 2022 at 8:34 PM Waldek Hebisch
> > > <[email protected]> wrote:
> > > >
> > > > 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).
> > >
> > > Do you mean to say that you cannot have ssh authentication with
> > > GitHub's git server?
> > > (well, yes, if you don't have a GitHub account then you can't upload
> > > an ssh key, indeed...)
> >
> > I have. But doing
> >
> > git clone https://github.com/fricas/fricas
> >
> > gives read-only copy. IIRC has to do use
> >
> > [email protected]:fricas/fricas
>
> Are you saying that
>
> git clone [email protected]:fricas/fricas
>
> does not work for you, despite having an ssh key uploaded?
That one works. But the is still question what address should
I use to fetch branch corresponding to pull request?
--
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/20220726182944.GA9154%40fricas.math.uni.wroc.pl.
