# HG changeset patch
# User wenzelm
# Date 1219862185 -7200
# Node ID dad9a2f178acf260fde45d556d63d5a61009e0f9
# Parent  d9fcab768496b14e09f7446a832be92432b495f1
load buffer.ML before file.ML;

diff -r d9fcab768496 -r dad9a2f178ac src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Wed Aug 27 20:36:23 2008 +0200
+++ b/src/Pure/General/ROOT.ML	Wed Aug 27 20:36:25 2008 +0200
@@ -30,8 +30,8 @@
 use "susp.ML";
 use "path.ML";
 use "url.ML";
+use "buffer.ML";
 use "file.ML";
-use "buffer.ML";
 use "xml.ML";
 use "yxml.ML";