doc-src/TutorialI/settings.ML
changeset 41197 edab1efe0a70
parent 38767 d8da44a8dd25