modernized generated example session;
authorwenzelm
Fri, 31 Jul 2009 11:34:14 +0200
changeset 32299 5f33ce0ed21f
parent 32294 d00238af17b6
child 32300 ad33af3242f3
modernized generated example session;
lib/Tools/mkdir
--- 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