equal
deleted
inserted
replaced
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 |