src/Pure/ROOT
changeset 50450 358b6020f8b6
parent 50255 d0ec1f0d1d7d
child 50686 d703e3aafa8c
--- a/src/Pure/ROOT	Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Pure/ROOT	Mon Dec 10 13:52:33 2012 +0100
@@ -144,11 +144,11 @@
     "ML/ml_statistics_polyml-5.5.0.ML"
     "ML/ml_syntax.ML"
     "ML/ml_thms.ML"
+    "PIDE/active.ML"
     "PIDE/command.ML"
     "PIDE/document.ML"
     "PIDE/markup.ML"
     "PIDE/protocol.ML"
-    "PIDE/sendback.ML"
     "PIDE/xml.ML"
     "PIDE/yxml.ML"
     "Proof/extraction.ML"