diff -r dda237f1d299 -r df7c3b1f390a src/Cube/ex/ROOT.ML
--- a/src/Cube/ex/ROOT.ML	Mon Sep 05 17:38:15 2005 +0200
+++ b/src/Cube/ex/ROOT.ML	Mon Sep 05 17:38:17 2005 +0200
@@ -1,2 +1,4 @@
+
+(* $Id$ *)
 
 time_use_thy "ex";