Panama repo closed for pushes

[Maurizio Cimadamore]

The corruption issue should have been addressed. New clones of 
panama/dev should no longer be affected by this.

If you have a local repository which is corrupted and would like to fix 
it, the standard way to fix it would be to clone the local repository 
into a new repository (local clones are fast) to changeset 57288, then 
pull remaining from panama/dev.

Thanks for the cooperation.
Maurizio

On 29/07/2019 10:06, Maurizio Cimadamore wrote:
> Hi,
> we will attempt to resolve the repository corruption issue later 
> today. In the meantime I kindly ask all interested parties to please 
> refrain from pushing any code to panama/dev, regardless of the branch.
>
> I will update as soon as the repo becomes available again.
>
> Thanks for the patience
> Maurizio
>