doc-src/TutorialI/settings.ML
author wenzelm
Wed, 25 Jan 2012 15:39:08 +0100
changeset 46256 bc874d2ee55a
parent 38767 d8da44a8dd25
permissions -rw-r--r--
updated RSN, RL, RLN, MRS; discontinued obscure MRL;

Thy_Output.indent_default := 5;