Hi Waldek,
The following is similar to what Qian suggested, but using ssh.
Create an ssh key and upload the ~/.ssh/github.pub to your github account.
ssh-keygen -t ecdsa -f $HOME/.ssh/github -C YOURNAME@github
Put the following into your ~/.ssh/config file
------------------------------------
# Access my github repositories.
Host github
IdentityFile ~/.ssh/github
HostName github.com
User git
------------------------------------
Get you personal FriCAS repository (that "remote" is called "origin" by
default.)
git clone github:hemmecke/fricas.git
Add the official FriCAS repo as "upstream"
git remote add upstream github:fricas/fricas.git
Both "origin" and "upstream" are writable, because you use ssh.
Get the pull request branch.
For example, to get https://github.com/fricas/fricas/pull/73 into your
local repository do the following.
git fetch upstream pull/73/head:pr-73
Now merge the pull request if you want
git merge pr-73
Push it to your own repo (if you like).
git push origin master
Push the new master to the official fricas repo.
git push upstream master
Ralf
--
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/f2374990-c398-197c-d69d-5fa9148c1724%40hemmecke.org.
