git push fails after moving remote repository on same server-CodePudding

I've got a git working repo and a bare repo on the same server as follows:

/
 ---dev
|     ---work
|    |    |   
|    |     ---.git
|    |     ---src
|    |     ---...
|    |
|     ---bare-repo.git
|
 ---other

Pushing and pulling from the work repo to the bare repo was working fine. Then I had the need to reorganise the directories like this:

/
 ---dev
|     ---work
|    |    |   
|    |     ---.git
|    |     ---src
|    |     ---...
|
 ---git
|     ---bare-repo.git
|
 ---other

While in /dev/work I changed the remote URL with:

git remote set-url origin /git/bare-repo.git

This command succeeded, but when I trying to push I'm getting:

fatal: '../bare-repo.git' does not appear to be a git repository
fatal: Could not read from remote repository.

Interesting. While git remote -v shows

origin  /git/bare-repo.git (fetch)
origin  /git/bare-repo.git (push)

the git config file contains:

[core]
    repositoryformatversion = 0
    filemode = true
    bare = false
    logallrefupdates = true
[branch "master"]
    remote = ../bare-repo.git
    merge = refs/heads/master
[remote "origin"]
    url = /git/bare.repo.git
    fetch =  refs/heads/*:refs/remotes/origin/*

So, the set-url did not change the remote for branch master. Should it? I guess, no. So the command I've found to change the URL of the remote 'origin' was not the best. I can edit the config file and correct the path manually, I suppose, but what would have been the correct procedure?

CodePudding user response：

I don't know how this happened:

[branch "master"]
    remote = ../bare-repo.git
    merge = refs/heads/master

but the middle line should read:

    remote = origin

With that fixed, everything else should Just Work.