changeset 75686 | 42f19e398ee4 |
parent 75682 | b6f3db86f9c7 |
child 75691 | 041d7d633977 |
--- a/src/Pure/ROOT.ML Thu Jul 21 15:01:48 2022 +0200 +++ b/src/Pure/ROOT.ML Fri Jul 22 15:15:26 2022 +0200 @@ -363,5 +363,5 @@ ML_file "Tools/doc.ML"; ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; +ML_file "Tools/scala_build.ML"; ML_file "Tools/generated_files.ML"; -ML_file "Tools/scala_build.ML";