doc-src/TutorialI/settings.ML
changeset 37216 3165bc303f66
parent 22097 7ee0529c5674
child 38767 d8da44a8dd25
equal deleted inserted replaced
37215:91dfe7dccfdf 37216:3165bc303f66
     1 (* $Id$ *)
     1 (* $Id$ *)
     2 
     2 
     3 ThyOutput.indent := 5;
     3 Thy_Output.indent := 5;