--- Makefile.sav	Tue Nov 12 21:23:27 2002
+++ Makefile	Fri Apr 25 16:00:50 2003
@@ -320,7 +320,8 @@
 full-small:   TAGS check
 	rm -f workxxx
 	rm -f acl2-fns.o acl2-fns.lbin acl2-fns.sbin acl2-fns.fasl acl2-fns.wfasl \
-	  acl2-fns.fas acl2-fns.lib acl2-fns.sparcf acl2-fns.ufsl acl2-fns.x86f
+	  acl2-fns.fas acl2-fns.lib acl2-fns.sparcf acl2-fns.ufsl acl2-fns.x86f \
+	  acl2-fns.dfsl
 	echo '(load "init.lsp")' > workxxx
 	echo '(acl2::compile-acl2 t)' >> workxxx
 	echo '(acl2::exit-lisp)' >> workxxx