lib/Tools/mkdir
changeset 8475 deb604b3d9a9
parent 8289 5b288a96bc61
child 8488 58e37d59c146
equal deleted inserted replaced
8474:ae32be343647 8475:deb604b3d9a9
   121     echo "## global settings"
   121     echo "## global settings"
   122     echo
   122     echo
   123     echo "SRC = \$(ISABELLE_HOME)/src"
   123     echo "SRC = \$(ISABELLE_HOME)/src"
   124     echo "OUT = \$(ISABELLE_OUTPUT)"
   124     echo "OUT = \$(ISABELLE_OUTPUT)"
   125     echo "LOG = \$(OUT)/log"
   125     echo "LOG = \$(OUT)/log"
   126     echo "USEDIR = \$(ISATOOL) usedir -i true -d dvi"
   126     echo "USEDIR = \$(ISATOOL) usedir -i true -d dvi  ## -D document"
   127     echo
   127     echo
   128     echo
   128     echo
   129     echo "## $NAME"
   129     echo "## $NAME"
   130     echo ""
   130     echo ""
   131     if [ -n "$PARENT" ]; then
   131     if [ -n "$PARENT" ]; then