# HG changeset patch # User clasohm # Date 803043534 -7200 # Node ID 75caf28a3aa907cdf6e19e646fbff4aad7b0a12c # Parent d25b863ab2acf817f0265afa16cf740fbda7a47b added CHOL diff -r d25b863ab2ac -r 75caf28a3aa9 src/Tools/make-all --- a/src/Tools/make-all Mon Jun 12 15:01:03 1995 +0200 +++ b/src/Tools/make-all Tue Jun 13 13:38:54 1995 +0200 @@ -54,7 +54,7 @@ echo Log files will be called make$$.log.gz case $FORCE.$EXEC in - on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL HOLCF Cube FOLP) + on.on) (cd $ISABELLEBIN; rm -f Pure FOL ZF CCL LCF CTT LK Modal HOL CHOL HOLCF Cube FOLP) esac set +e #no longer fail upon errors -- e.g. if a "make" fails @@ -152,6 +152,16 @@ echo echo +echo '*****Curried Higher-Order Logic (CHOL)*****' +(cd CHOL; make $NO $TEST > make$$.log) +tail CHOL/make$$.log +gzip CHOL/make$$.log +case $CLEAN.$EXEC in + on.on) rm $ISABELLEBIN/CHOL +esac + +echo +echo echo '*****The Lambda-Cube (Cube)*****' (cd Cube; make $NO $TEST > make$$.log) case $CLEAN.$EXEC in @@ -174,7 +184,7 @@ test.on) echo echo '***** Now check the dates on the "test" files *****' ls -lrt FOL/test ZF/test CCL/test LCF/test CTT/test\ - LK/test Modal/test HOL/test HOLCF/test Cube/test\ - FOLP/test + LK/test Modal/test HOL/test CHOL/test HOLCF/test\ + Cube/test FOLP/test esac echo Finished at `date`