doc-src/TutorialI/settings.ML
changeset 40232 7ed03c0ae420
parent 38767 d8da44a8dd25
equal deleted inserted replaced
40231:997d6fb439a9 40232:7ed03c0ae420