doc-src/TutorialI/settings.ML
changeset 43573 81f7dca3e542
parent 38767 d8da44a8dd25
equal deleted inserted replaced
43572:ae612a423dad 43573:81f7dca3e542