doc-src/TutorialI/settings.ML
changeset 45124 d78ec6c10fa1
parent 38767 d8da44a8dd25
equal deleted inserted replaced
45122:49e305100097 45124:d78ec6c10fa1