[isabelle-dev] Concerning AFP 2a0f81020af9
lammich at in.tum.de
Thu Oct 31 08:55:51 CET 2013
Oops, that was me! Sorry, it was a test of mine, that I obviously forgot
The whole export_code - block can be removed, I'll do it in afp-devel,
but someone has to remove it in the snapshot.
On Do, 2013-10-31 at 08:44 +0100, Florian Haftmann wrote:
> In thys/JinjaThreads/Examples/ApprenticeChallenge.thy:
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev