src/Pure/ROOT.ML
changeset 68090 7c8ed28dd40a
parent 67588 f3a68e350ab6
child 68154 42d63ea39161
     1.1 --- a/src/Pure/ROOT.ML	Sun May 06 19:10:21 2018 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Sun May 06 22:15:52 2018 +0200
     1.3 @@ -300,6 +300,7 @@
     1.4  ML_file "PIDE/command.ML";
     1.5  ML_file "PIDE/query_operation.ML";
     1.6  ML_file "PIDE/resources.ML";
     1.7 +ML_file "Thy/export.ML";
     1.8  ML_file "Thy/present.ML";
     1.9  ML_file "Thy/thy_info.ML";
    1.10  ML_file "Thy/sessions.ML";