--- a/doc-src/TutorialI/settings.ML Fri Aug 27 00:09:56 2010 +0200 +++ b/doc-src/TutorialI/settings.ML Fri Aug 27 12:40:20 2010 +0200 @@ -1,3 +1,1 @@ -(* $Id$ *) - -Thy_Output.indent := 5; +Thy_Output.indent_default := 5;