doc-src/TutorialI/settings.ML
changeset 42490 3633ecaaf3ef
parent 38767 d8da44a8dd25
equal deleted inserted replaced
42489:db9b9e46131c 42490:3633ecaaf3ef