lib/Tools/mkdir
changeset 8579 81ef0fc80822
parent 8501 2ff3d25943f1
child 8685 05b6e5bcab66
     1.1 --- a/lib/Tools/mkdir	Sat Mar 25 18:01:27 2000 +0100
     1.2 +++ b/lib/Tools/mkdir	Sun Mar 26 20:08:03 2000 +0200
     1.3 @@ -94,6 +94,7 @@
     1.4    TEST=""
     1.5    TARGET="\$(OUT)/$NAME"
     1.6    ROOT_ML="ROOT.ML"
     1.7 +  SOURCES="*.thy"
     1.8    [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="document/root.tex"
     1.9    USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
    1.10  else
    1.11 @@ -101,6 +102,7 @@
    1.12    TEST="$NAME"
    1.13    TARGET="\$(LOG)/$LOGIC-$NAME.gz"
    1.14    ROOT_ML="$NAME/ROOT.ML"
    1.15 +  SOURCES="$NAME/*.thy"
    1.16    [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="$NAME/document/root.tex"
    1.17    USEDIR="\$(USEDIR)"
    1.18  fi
    1.19 @@ -134,12 +136,12 @@
    1.20        echo "$LOGIC:"
    1.21        echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
    1.22        echo
    1.23 -      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT  ## add $NAME sources here"
    1.24 +      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT  ## $SOURCES"
    1.25        echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
    1.26      else
    1.27        echo "$NAME: $TARGET"
    1.28        echo
    1.29 -      echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT  ## add $NAME sources here"
    1.30 +      echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT  ## $SOURCES"
    1.31        echo -e "\t@$USEDIR $LOGIC $NAME"
    1.32      fi
    1.33      echo