[isabelle-dev] Concerning AFP 2a0f81020af9

[Peter Lammich]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev