doc-src/TutorialI/settings.ML
author blanchet
Mon, 09 Jul 2012 23:23:12 +0200
changeset 48216 9075d4636dd8
parent 38767 d8da44a8dd25
permissions -rw-r--r--
generate problem file

Thy_Output.indent_default := 5;