doc-src/TutorialI/settings.ML
changeset 14772 c52060b69a8c
parent 9834 109b11c4e77e
child 22097 7ee0529c5674
equal deleted inserted replaced
14771:c2bf21b5564e 14772:c52060b69a8c