IIUC, there are two ways according to
https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/reviewing-changes-in-pull-requests/checking-out-pull-requests-locally
1. Use github-cli. Pretty big package, written in go.
I never used it.
2. "Fetch the reference to the pull request based on its ID number,
creating a new branch in the process."
````
$ git fetch origin pull/ID/head:BRANCHNAME
````
For example:
````
git fetch origin pull/100/head:pr-100
````
Creates a local branch "pr-100" that references
https://github.com/fricas/fricas/pull/100
- Qian
On 7/27/22 02:29, Waldek Hebisch wrote:
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?
--
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/5b15c308-3ee4-58ec-36ef-b82ff66a2841%40gmail.com.
