Yes, after the pull, cleaning, then making would have to be done. I believe everyone wass aware of that but the concern here was how to switch grom a lagging repo to the more up to date repo for the pull.
On Wednesday, October 26, 2011, Dave Abrahams <d...@boostpro.com> wrote: > > on Wed Oct 26 2011, suvayu ali <fatkasuvayu+linux-AT-gmail.com> wrote: > >> 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. > > Not if there were compiled files. > > -- > Dave Abrahams > BoostPro Computing > http://www.boostpro.com > > >
