doc-src/TutorialI/settings.ML
changeset 33387 acea2f336721
parent 22097 7ee0529c5674
child 37216 3165bc303f66
equal deleted inserted replaced
33386:ff29d1549aca 33387:acea2f336721