doc-src/TutorialI/settings.ML
changeset 41017 666d8ed0b73a
parent 38767 d8da44a8dd25
equal deleted inserted replaced
41016:343cdf923c02 41017:666d8ed0b73a