[isabelle-dev] Fisher–Yates in AFP

Johannes Hölzl hoelzl at in.tum.de
Tue Oct 4 13:24:01 CEST 2016


You may want to use

  hg archive ~/Fishe-Yates.tar.gz

in the future.

  - Johannes

Am Dienstag, den 04.10.2016, 13:18 +0200 schrieb Manuel Eberl:
> Oh, that is quite possible. Sorry about that. I typically keep my
> prospective AFP entries in private HG repositories and then simply
> tarball and submit them when it's time. I don't think that ever was a
> problem before, but it sounds like the most reasonably explanation so
> far.
> Good catch!
> Manuel
> 
> On 04/10/16 13:16, Lars Hupel wrote:
> > > It isn’t only about SourceTree. As I mentioned, manually adding
> > > Fisher_Yates had no effect, and even now "hg diff” shows nothing,
> > > even though Fisher_Yates should appear as “added” or untracked
> > > (given that it’s on my machine and nowhere else). I’ve also
> > > checked every .hgignore file.
> > > 
> > > Possibly my copy of the AFP has got corrupted somehow.
> > I just checked the submission Manuel uploaded to the submission
> > system
> > and there seems to be an extra ".hg" folder in there. So possibly
> > Mercurial ignores that directory. It might get fixed by "rm -rf"ing
> > that
> > extra folder.
> > 
> > Cheers
> > Lars
>  
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev



More information about the isabelle-dev mailing list