# HG changeset patch
# User wenzelm
# Date 1249079985 -7200
# Node ID ad33af3242f30c72c85bad4c241754748a5c96ed
# Parent  e6a8ed8aed3ad61e7f3bbf6060b6683136086a81# Parent  5f33ce0ed21f3402b2c29668c87bae74dc6f0328
merged

diff -r e6a8ed8aed3a -r ad33af3242f3 lib/Tools/mkdir
--- a/lib/Tools/mkdir	Sat Aug 01 00:17:03 2009 +0200
+++ b/lib/Tools/mkdir	Sat Aug 01 00:39:45 2009 +0200
@@ -187,8 +187,8 @@
   [ -z "$QUIET" ] && echo "creating $PREFIX/ROOT.ML" >&2
   cat >ROOT.ML <<EOF
 (*
-  no_document use_thy "ThisTheory";
-  use_thy "ThatTheory";
+  no_document use_thys ["This_Theory1", "This_Theory2"];
+  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
 *)
 EOF
 fi