src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Tue Oct 18 15:31:08 2016 +0200
+++ b/src/Pure/ROOT.ML	Tue Oct 18 16:03:30 2016 +0200
@@ -67,6 +67,7 @@
 ML_file "PIDE/xml.ML";
 ML_file "General/path.ML";
 ML_file "General/url.ML";
+ML_file "System/bash_syntax.ML";
 ML_file "General/file.ML";
 ML_file "General/long_name.ML";
 ML_file "General/binding.ML";