doc-src/TutorialI/settings.ML
changeset 25518 00d5cc16e891
parent 22097 7ee0529c5674
child 37216 3165bc303f66
equal deleted inserted replaced
25517:36d710d1dbce 25518:00d5cc16e891