equal
deleted
inserted
replaced
136 echo |
136 echo |
137 echo "SRC = \$(ISABELLE_HOME)/src" |
137 echo "SRC = \$(ISABELLE_HOME)/src" |
138 echo "OUT = \$(ISABELLE_OUTPUT)" |
138 echo "OUT = \$(ISABELLE_OUTPUT)" |
139 echo "LOG = \$(OUT)/log" |
139 echo "LOG = \$(OUT)/log" |
140 echo |
140 echo |
141 echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d dvi ## -D document" |
141 echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d dvi ## -D generated" |
142 echo |
142 echo |
143 echo |
143 echo |
144 echo "## $NAME" |
144 echo "## $NAME" |
145 echo "" |
145 echo "" |
146 if [ -n "$PARENT" ]; then |
146 if [ -n "$PARENT" ]; then |