| changeset 71397 | 028edb1e5b99 |
| parent 71396 | c1c61d0d8e7c |
| child 72131 | 284d6c06cbfb |
--- a/Admin/polyml/settings Sun Jan 19 14:23:49 2020 +0100 +++ b/Admin/polyml/settings Sun Jan 19 14:50:03 2020 +0100 @@ -16,4 +16,4 @@ ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_SOURCES="$POLYML_HOME/src" -ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:$POLYML_HOME/src/ROOT.ML" +ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT.ML"