doc-src/TutorialI/settings.ML
author bulwahn
Wed, 30 Mar 2011 19:09:57 +0200
changeset 42176 c7b6d8d9922e
parent 38767 d8da44a8dd25
permissions -rw-r--r--
removing dead code in exhaustive_generators

Thy_Output.indent_default := 5;