# 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";