diff -r 3b9e3c782eb2 -r 81ef0fc80822 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