| changeset 75660 | 45d3497c0baa |
| parent 75621 | aeb412065742 |
| child 75682 | b6f3db86f9c7 |
--- a/src/Pure/ROOT.ML Fri Jul 08 20:24:05 2022 +0200 +++ b/src/Pure/ROOT.ML Fri Jul 08 22:29:26 2022 +0200 @@ -362,4 +362,5 @@ ML_file "Tools/doc.ML"; ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; -ML_file "Tools/generated_files.ML" +ML_file "Tools/generated_files.ML"; +ML_file "Tools/scala_build.ML";