diff -r d7f8ee80ad42 -r c1c61d0d8e7c Admin/polyml/settings
--- 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"