[isabelle-dev] Fisher–Yates in AFP

Manuel Eberl eberlm at in.tum.de
Tue Oct 4 13:18:58 CEST 2016

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!


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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161004/af0ab57f/attachment-0002.html>

More information about the isabelle-dev mailing list