[isabelle-dev] Formal dependency on "poly" executable

Makarius makarius at sketis.net
Wed Nov 8 18:05:22 CET 2017

See now:

changeset:   67033:09fb749d1a1e
user:        wenzelm
date:        Wed Nov 08 17:34:32 2017 +0100
files:       src/Pure/Pure.thy
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

The $POLYML_EXE is from Isabelle/8176914dae84. When testing older
Poly/ML versions, POLYML_EXE="$ML_HOME/poly" is required in


More information about the isabelle-dev mailing list