doc-src/TutorialI/settings.ML
changeset 36057 ca6610908ae9
parent 22097 7ee0529c5674
child 37216 3165bc303f66
equal deleted inserted replaced
36056:0c128c2c310d 36057:ca6610908ae9