src/Pure/ROOT.ML
changeset 64304 96bc94c87a81
parent 63932 6040db6b929d
child 65505 741fad555d82
     1.1 --- a/src/Pure/ROOT.ML	Tue Oct 18 15:31:08 2016 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Oct 18 16:03:30 2016 +0200
     1.3 @@ -67,6 +67,7 @@
     1.4  ML_file "PIDE/xml.ML";
     1.5  ML_file "General/path.ML";
     1.6  ML_file "General/url.ML";
     1.7 +ML_file "System/bash_syntax.ML";
     1.8  ML_file "General/file.ML";
     1.9  ML_file "General/long_name.ML";
    1.10  ML_file "General/binding.ML";