doc-src/TutorialI/settings.ML
changeset 23940 f2181804fced
parent 22097 7ee0529c5674
child 37216 3165bc303f66
equal deleted inserted replaced
23939:e543359fe8b6 23940:f2181804fced