src/Pure/ROOT.ML
changeset 50800 c0fb2839d1a9
parent 50757 37091451ba1a
child 50911 ee7fe4230642
     1.1 --- a/src/Pure/ROOT.ML	Wed Jan 09 22:38:21 2013 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Thu Jan 10 12:41:53 2013 +0100
     1.3 @@ -57,6 +57,7 @@
     1.4  use "General/file.ML";
     1.5  use "General/long_name.ML";
     1.6  use "General/binding.ML";
     1.7 +use "General/socket_io.ML";
     1.8  
     1.9  use "General/sha1.ML";
    1.10  if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();