See now:
changeset: 67033:09fb749d1a1e
user: wenzelm
date: Wed Nov 08 17:34:32 2017 +0100
files: src/Pure/Pure.thy
description:
formal dependency on "poly" executable;
I've myself got into problems finding odd spaces to remove from Pure ML
sources, in order to force a rebuild after changing the Poly/ML test
version.
The $POLYML_EXE is from Isabelle/8176914dae84. When testing older
Poly/ML versions, POLYML_EXE="$ML_HOME/poly" is required in
$ISABELLE_HOME_USER/etc/settings.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
