load buffer.ML before file.ML;
authorwenzelm
Wed, 27 Aug 2008 20:36:25 +0200
changeset 28026 dad9a2f178ac
parent 28025 d9fcab768496
child 28027 051d5ccbafc5
load buffer.ML before file.ML;
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";