Re: BUG #6722: Debugger broken?

On Mon, Aug 13, 2012 at 1:51 PM, Craig Ringer <ringerc@ringerc.id.au> wrote:
> On 08/13/2012 07:19 PM, Heikki Linnakangas wrote:
>
>>
>> I tried to drop and recreate the branch, but the server would not let me
>> push that change, as it's a non-fast-forward update. Someone needs to
>> temporarily remove the check for that from the git server - I don't think I
>> have access to do that. Do you?
>>
>
> pushing with --force didn't work?
>
> git push --force origin mybranch

Yeah, there is nothing on the git server that should stop you from
doing a force push, I believe.

There are rules in place to stop it from pushing merge commits, if
that has been enabled. But there are no such rules enabled for the
pldebugger one.

Note of course, which you probably already know, that doing a force
push may cause problems for others who have cloned the repository...

--
 Magnus Hagander
 Me: http://www.hagander.net/
 Work: http://www.redpill-linpro.com/