doc-src/TutorialI/settings.ML
author haftmann
Fri, 16 Mar 2012 22:26:55 +0100
changeset 46980 6bc213e90401
parent 38767 d8da44a8dd25
permissions -rw-r--r--
tuned specifications

Thy_Output.indent_default := 5;