[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
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
More information about the isabelle-dev
mailing list