On 31 Oct 2013, at 9:04 pm, Peter Lammich <[email protected]> wrote:
> On Do, 2013-10-31 at 10:57 +0100, Florian Haftmann wrote: >>> The whole export_code - block can be removed, I'll do it in afp-devel, >> >> Thanks. >> >>> but someone has to remove it in the snapshot. > > I meant the release branch of AFP, that Gerwin made a few days ago. See > also: > > https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-October/004787.html Yes. I’ll move the patch over. Cheers, Gerwin
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
