basic source deps;
authorwenzelm
Mon Feb 14 20:49:08 2000 +0100 (2000-02-14)
changeset 8244c587f5ac4a98
parent 8243 5db67376df7d
child 8245 6acc80f7f36f
basic source deps;
lib/Tools/mkdir
     1.1 --- a/lib/Tools/mkdir	Mon Feb 14 20:43:12 2000 +0100
     1.2 +++ b/lib/Tools/mkdir	Mon Feb 14 20:49:08 2000 +0100
     1.3 @@ -87,15 +87,21 @@
     1.4  
     1.5  # IsaMakefile
     1.6  
     1.7 +DOCUMENT_ROOT=""
     1.8 +
     1.9  if [ -n "$BUILD" ]; then
    1.10    IMAGES="$NAME"
    1.11    TEST=""
    1.12    TARGET="\$(OUT)/$NAME"
    1.13 +  ROOT_ML="ROOT.ML"
    1.14 +  [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="document/root.tex"
    1.15    USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
    1.16  else
    1.17    IMAGES=""
    1.18    TEST="$NAME"
    1.19    TARGET="\$(LOG)/$LOGIC-$NAME.gz"
    1.20 +  ROOT_ML="$NAME/ROOT.ML"
    1.21 +  [ -n "$DOCUMENT" ] && DOCUMENT_ROOT="$NAME/document/root.tex"
    1.22    USEDIR="\$(USEDIR)"
    1.23  fi
    1.24  
    1.25 @@ -128,12 +134,12 @@
    1.26        echo "$LOGIC:"
    1.27        echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
    1.28        echo
    1.29 -      echo "$TARGET: \$(OUT)/$LOGIC     ## add $NAME sources here"
    1.30 +      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT  ## add $NAME sources here"
    1.31        echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
    1.32      else
    1.33        echo "$NAME: $TARGET"
    1.34        echo
    1.35 -      echo "$TARGET:                    ## add $NAME sources here"
    1.36 +      echo "$TARGET: $ROOT_ML $DOCUMENT_ROOT  ## add $NAME sources here"
    1.37        echo -e "\t@$USEDIR $LOGIC $NAME"
    1.38      fi
    1.39      echo