[isabelle-dev] Fisher–Yates in AFP

Lawrence Paulson lp15 at cam.ac.uk
Tue Oct 4 13:21:08 CEST 2016

That is indeed the culprit.

If it’s no problem, maybe the submission system could check for such directories and delete them?


> On 4 Oct 2016, at 12:18, Manuel Eberl <eberlm at in.tum.de> wrote:
> 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!

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

More information about the isabelle-dev mailing list