doc-src/TutorialI/settings.ML
changeset 26021 25d06476727e
parent 22097 7ee0529c5674
child 37216 3165bc303f66
equal deleted inserted replaced
26020:ffe1a032d24b 26021:25d06476727e