doc-src/TutorialI/settings.ML
changeset 38767 d8da44a8dd25
parent 37216 3165bc303f66
equal deleted inserted replaced
38766:8891f4520d16 38767:d8da44a8dd25
     1 (* $Id$ *)
     1 Thy_Output.indent_default := 5;
     2 
       
     3 Thy_Output.indent := 5;