tuned targets;
authorwenzelm
Sun, 26 Mar 2000 20:08:03 +0200
changeset 8579 81ef0fc80822
parent 8578 3b9e3c782eb2
child 8580 e79ee31d3936
tuned targets;
lib/Tools/mkdir
--- a/lib/Tools/mkdir	Sat Mar 25 18:01:27 2000 +0100
+++ b/lib/Tools/mkdir	Sun Mar 26 20:08:03 2000 +0200
@@ -94,6 +94,7 @@
   TEST=""
   TARGET="\$(OUT)/$NAME"
   ROOT_ML="ROOT.ML"
+  SOURCES="*.thy"
   [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="document/root.tex"
   USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
 else
@@ -101,6 +102,7 @@
   TEST="$NAME"
   TARGET="\$(LOG)/$LOGIC-$NAME.gz"
   ROOT_ML="$NAME/ROOT.ML"
+  SOURCES="$NAME/*.thy"
   [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="$NAME/document/root.tex"
   USEDIR="\$(USEDIR)"
 fi
@@ -134,12 +136,12 @@
       echo "$LOGIC:"
       echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
       echo
-      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT  ## add $NAME sources here"
+      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT  ## $SOURCES"
       echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
     else
       echo "$NAME: $TARGET"
       echo
-      echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT  ## add $NAME sources here"
+      echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT  ## $SOURCES"
       echo -e "\t@$USEDIR $LOGIC $NAME"
     fi
     echo