diff -r 3441647c8c90 -r 024b242bc26f make-all --- a/make-all Thu Feb 03 14:00:36 1994 +0100 +++ b/make-all Thu Feb 03 16:06:55 1994 +0100 @@ -142,7 +142,7 @@ echo echo -echo '*****LCF in HOL (HOL)*****' +echo '*****LCF in HOL (HOLCF)*****' (cd HOLCF; make $NO $TEST > make$$.log) tail HOLCF/make$$.log gzip HOLCF/make$$.log