| 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"