Oops, that was me! Sorry, it was a test of mine, that I obviously forgot to remove.
The whole export_code - block can be removed, I'll do it in afp-devel, but someone has to remove it in the snapshot. -- Peter On Do, 2013-10-31 at 08:44 +0100, Florian Haftmann wrote: > In thys/JinjaThreads/Examples/ApprenticeChallenge.thy: > > export_code > ApprenticeChallenge_annotated > exec_J_rr > J2JVM > Apprentice > main > Null > exec_JVM_rr > in SML module_name JT file "/tmp/NEW" > ^^^^^^^^^^ > > This is definitely not nice, especially in a shared environment like the > NFS at TUM where currently lxbroy10:/tmp/NEW is blocked. > > What is the intention of this? A mere check could be done also > export_code … checking or at least referring to $ISABELLE_TMP_PREFIX. > > Florian > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev