[Taler] (docs) mistaken branch

[Thien-Thi Nguyen]

I accidentally pushed branch ‘p’ to the docs.git repo.  When i
try to delete it, i see:

| $ git push taler :p
| remote: refs/heads/p 8b8fa591fce11d1763cd94c90a746cac4550ea8a 
0000000000000000000000000000000000000000        
| remote: A force-push or delete is only possible for branches named 
'dev/USER/...'.        
| remote: Admins are excluded from this policy, please ask them if you really 
have to delete a branch.        
| remote: 
| remote: FATAL -- ACCESS DENIED        
| remote: Repo            docs                                                  
              
| remote: User            ttn                                                   
              
| remote: Stage           From git's update hook                                
              
| remote: Ref             VREF 'FORBIDDEN_FORCE_PUSH'                           
              
| remote: Operation       Rewind push branch or overwrite tag                   
              
| remote: 
| remote: FATAL: + VREF/FORBIDDEN_FORCE_PUSH docs ttn DENIED by 
VREF/FORBIDDEN_FORCE_PUSH        
| remote: error: hook declined to update refs/heads/p        
| To git+ssh://git.taler.net/docs.git
|  ! [remote rejected] p (hook declined)
| error: push di alcuni riferimenti su 'git+ssh://git.taler.net/docs.git' non 
riuscito

Could someone please delete this branch for me?

Thanks in advance and sorry for the mishap.

-- 
Thien-Thi Nguyen -----------------------------------------------
 (defun responsep (query)               ; (2020) Software Libero
   (pcase (context query)               ;       = Dissenso Etico
     (`(technical ,ml) (correctp ml))
     ...))                              748E A0E8 1CB8 A748 9BFA
--------------------------------------- 6CE4 6703 2224 4C80 7502

signature.asc
Description: PGP signature