I shall have to file this one under “mercurial mysteries”, which is already a supermassive black hole.
I got the push to work, now I’m hoping I don’t have to touch it again for a long time. Larry > On 21 Feb 2017, at 21:56, Blanchette, J.C. <j.c.blanche...@vu.nl> wrote: > > >> On 21.02.2017, at 22:12, Lawrence Paulson <l...@cam.ac.uk >> <mailto:l...@cam.ac.uk>> wrote: >> >> I committed some changes (fixing AFP-devel), which I would like to push. But >> what in God’s name is this? >> >> ~/isabelle/afp/devel/thys: hg push >> pushing to https://bitbucket.org/isa-afp/afp-devel >> <https://bitbucket.org/isa-afp/afp-devel> > > In your ~/isabelle/afp/devel/.hg/hgrc, I presume there's a line that looks > like this: > > default = https://bitbucket.org/isa-afp/afp-devel > <https://bitbucket.org/isa-afp/afp-devel> > > Change it to > > default = ssh://h...@bitbucket.org/isa-afp/afp-devel > <ssh://h...@bitbucket.org/isa-afp/afp-devel> > Jasmin >
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev