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
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
