equal
deleted
inserted
replaced
140 gzip HOL/make$$.log |
140 gzip HOL/make$$.log |
141 #cannot delete HOL yet... it is needed for HOLCF! |
141 #cannot delete HOL yet... it is needed for HOLCF! |
142 |
142 |
143 echo |
143 echo |
144 echo |
144 echo |
145 echo '*****LCF in HOL (HOL)*****' |
145 echo '*****LCF in HOL (HOLCF)*****' |
146 (cd HOLCF; make $NO $TEST > make$$.log) |
146 (cd HOLCF; make $NO $TEST > make$$.log) |
147 tail HOLCF/make$$.log |
147 tail HOLCF/make$$.log |
148 gzip HOLCF/make$$.log |
148 gzip HOLCF/make$$.log |
149 case $CLEAN.$EXEC in |
149 case $CLEAN.$EXEC in |
150 on.on) rm $ISABELLEBIN/HOL $ISABELLEBIN/HOLCF |
150 on.on) rm $ISABELLEBIN/HOL $ISABELLEBIN/HOLCF |