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 <dave@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.stengele@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
>
>
>