doc-src/TutorialI/settings.ML
author bulwahn
Thu, 21 Jun 2012 13:51:44 +0200
changeset 48111 33414f2e82ab
parent 38767 d8da44a8dd25
permissions -rw-r--r--
NEWS and CONTRIBUTORS

Thy_Output.indent_default := 5;