doc-src/TutorialI/settings.ML
changeset 16347 9b3265182607
parent 9834 109b11c4e77e
child 22097 7ee0529c5674
equal deleted inserted replaced
16346:baa7b5324fc1 16347:9b3265182607