doc-src/TutorialI/settings.ML
changeset 30713 b1a87e3971a3
parent 22097 7ee0529c5674
child 37216 3165bc303f66
equal deleted inserted replaced
30712:fc9d8b1bf1e0 30713:b1a87e3971a3