On Sat, Sep 22, 2012 at 06:05:34PM +0100, Alessandro Grassi wrote:
> How do I merge changes from the main repository to my repository on
> repo.or.cz? I think it should be:
> 
> git pull git://git.immerda.ch/amnesia.git
> git push <my_repository>
> 
> from a local copy of my repo on my PC. Is that correct?
Nope. :)
You need to add a remote first (here named 'upstream'):
    git remote add ustream git://git.immerda.ch/amnesia.git
And then you can pull from it:
    git pull upstream
But pull is actually fetch+merge. What I usually do perform the two
steps manually, usually looking up the logs first:
    git fetch upstream
    git log upstream/master
    git merge upstream/master
Hope that helps,
-- 
Ague