| changeset 32300 | ad33af3242f3 |
| parent 32299 | 5f33ce0ed21f |
| child 40895 | c3f68ea97495 |
--- 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