--- a/src/Pure/ROOT Thu Jul 11 12:28:24 2013 +0200 +++ b/src/Pure/ROOT Thu Jul 11 14:42:11 2013 +0200 @@ -150,6 +150,7 @@ "ML/ml_syntax.ML" "ML/ml_thms.ML" "PIDE/active.ML" + "PIDE/exec.ML" "PIDE/command.ML" "PIDE/document.ML" "PIDE/document_id.ML"