Re: feature/package-vc has been merged

[Philip Kaludercic]

Stefan Monnier <monnier@iro.umontreal.ca> writes:

>> (Btw, I am trying to force-push to the scratch branch but this appears
>> not to work.  Wasn't that the point of a scratch branch?)
>
> The repository does not allow force pushes.  There's no finer config as
> far as I know.  You can still technically force push to any branch by
> deleting the branch and pushing anew, i.e. something like:
>
>     git push origin :scratch/foo
>     git push origin HEAD:scratch/foo
>
> We only tolerate that in scratch/* branches, tho.

I suspected as much.  That is why I pushed the changes under that
branch.  Thanks for the clarification, I've pushed the changes.