src/Pure/ROOT
changeset 58928 23d0ffd48006
parent 58846 98c03412079b
child 59026 30b8a5825a9c
--- a/src/Pure/ROOT	Fri Nov 07 16:22:25 2014 +0100
+++ b/src/Pure/ROOT	Fri Nov 07 16:36:55 2014 +0100
@@ -154,6 +154,7 @@
     "ML/ml_compiler_polyml.ML"
     "ML/ml_context.ML"
     "ML/ml_env.ML"
+    "ML/ml_file.ML"
     "ML/ml_lex.ML"
     "ML/ml_parse.ML"
     "ML/ml_options.ML"