Rainer Stengele <rainer.steng...@online.de> wrote: > No, the old repo > > git://repo.or.cz/org-mode.git > > I used is some time behind the one I use now. > If I want to get a fix immediately I learned I have to use the new repo > git://orgmode.org/org-mode.git > > I hope I got this right. > > Rainer > > Am 26.10.2011 14:11, schrieb suvayu ali: > > On Wed, Oct 26, 2011 at 10:07, Rainer Stengele > > <rainer.steng...@online.de> wrote: > >> Lacking knowledge of git I deleted everything, cloned from the new repo > >> and compiled the files. > >> Result was a significantly faster Org experience. > >> > > For future reference, a sinple `git pull` would have sufficed. > > >
It's too late for it now, but for future reference: you can change the repo with ``git config --replace-all remote.origin.url git://orgmode.org/org-mode.git'' and then do a ``git pull''. AFAIK, the repo.or.cz/org-mode.git repo was a delayed mirror, so it would have the same history (up to the point of the latest sync). But it doesn't really matter: cloning the repo again takes longer but it's a one-time cost and the end result is the same. Nick