equal
deleted
inserted
replaced
54 echo Log files will be called make$$.log.gz |
54 echo Log files will be called make$$.log.gz |
55 |
55 |
56 case $FORCE.$EXEC in |
56 case $FORCE.$EXEC in |
57 on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL Cube FOLP) |
57 on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL Cube FOLP) |
58 esac |
58 esac |
|
59 |
|
60 set +e #no longer fail upon errors -- e.g. if a "make" fails |
59 |
61 |
60 echo |
62 echo |
61 echo |
63 echo |
62 echo '*****Pure Isabelle*****' |
64 echo '*****Pure Isabelle*****' |
63 (cd Pure; make $NO > make$$.log) |
65 (cd Pure; make $NO > make$$.log) |