doc-src/TutorialI/settings.ML
changeset 18145 6757627acf59
parent 9834 109b11c4e77e
child 22097 7ee0529c5674
equal deleted inserted replaced
18144:4edcb5fdc3b0 18145:6757627acf59