doc-src/TutorialI/settings.ML
author blanchet
Wed, 23 May 2012 13:37:26 +0200
changeset 47963 46c73ad5f7c0
parent 38767 d8da44a8dd25
permissions -rw-r--r--
doc updates

Thy_Output.indent_default := 5;