| changeset 71396 | c1c61d0d8e7c |
| parent 70988 | 38ade730f6df |
| child 71397 | 028edb1e5b99 |
--- a/Admin/polyml/settings Sun Jan 19 12:57:20 2020 +0100 +++ b/Admin/polyml/settings Sun Jan 19 14:23:49 2020 +0100 @@ -15,3 +15,5 @@ ML_SYSTEM=polyml-5.8.1 ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_SOURCES="$POLYML_HOME/src" + +ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:$POLYML_HOME/src/ROOT.ML"