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

[Makarius]

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