src/Pure/General/ROOT.ML
changeset 26077 1498f0362362
parent 25728 71e33d95ac55
child 26097 943582a2d1e2
--- a/src/Pure/General/ROOT.ML	Sat Feb 16 02:08:07 2008 +0100
+++ b/src/Pure/General/ROOT.ML	Sat Feb 16 16:43:53 2008 +0100
@@ -32,4 +32,5 @@
 use "buffer.ML";
 use "history.ML";
 use "xml.ML";
+use "system_process.ML";