address@hidden acl2-sources]$ 
address@hidden acl2-sources]$ time make certify-books ACL2=/home/bill/acl2-sources/debian-gnu-linux-gcl-saved_acl2.gcl 
cd books ; make
make[1]: Entering directory `/home/bill/acl2-sources/books'
Tue May 18 18:13:17 EDT 2004

.
.
.

make[2]: Leaving directory `/home/bill/acl2-sources/books'
27825.45user 157.89system 7:50:31elapsed 99%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (4946875major+3920895minor)pagefaults 0swaps
Wed May 19 02:03:49 EDT 2004
make[1]: Leaving directory `/home/bill/acl2-sources/books'
27825.54user 157.90system 7:50:31elapsed 99%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (4948129major+3921367minor)pagefaults 0swaps
address@hidden acl2-sources]$ 
address@hidden acl2-sources]$