author | wenzelm |
Fri, 31 Jul 2009 11:34:14 +0200 | |
changeset 32299 | 5f33ce0ed21f |
parent 32294 | d00238af17b6 |
child 32300 | ad33af3242f3 |
lib/Tools/mkdir | file | annotate | diff | comparison | revisions |
--- a/lib/Tools/mkdir Thu Jul 30 23:50:11 2009 +0200 +++ b/lib/Tools/mkdir Fri Jul 31 11:34:14 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