# HG changeset patch
# User haftmann
# Date 1281521037 -7200
# Node ID 749a3e6eb0f48a032583104c2f1ed91a3257d04b
# Parent  dc2a61b98bab5de24134789eae18cd77e8fd9742
added .ML extension

diff -r dc2a61b98bab -r 749a3e6eb0f4 doc-src/TutorialI/Fun/ROOT.ML
--- a/doc-src/TutorialI/Fun/ROOT.ML	Wed Aug 11 11:56:57 2010 +0200
+++ b/doc-src/TutorialI/Fun/ROOT.ML	Wed Aug 11 12:03:57 2010 +0200
@@ -1,2 +1,2 @@
-use "../settings";
+use "../settings.ML";
 use_thy "fun0";