doc-src/TutorialI/settings.ML
changeset 25533 0140cc7b26ad
parent 22097 7ee0529c5674
child 37216 3165bc303f66
equal deleted inserted replaced
25532:27f6771ae8fb 25533:0140cc7b26ad