Gaby,
Here is just a quick patch to make sure that all the
'stamp-*' directories are deleted in the case of
'make clean'.
--------
-sh-3.00$ diff -au Makefile.pamphlet_orig Makefile.pamphlet
--- Makefile.pamphlet_orig 2006-09-13 18:03:28.000000000 -0400
+++ Makefile.pamphlet 2006-09-13 18:06:58.000000000 -0400
@@ -94,7 +94,7 @@
@ rm -rf int
@ rm -rf obj
@ rm -rf mnt
- @ rm -f stamp-*
+ @ rm -f `find . -name 'stamp*'`
@ for i in `find . -name "*~"` ; do rm -f $$i ; done
@ for i in `find src -name "Makefile.dvi"` ; do rm -f $$i ; done
-sh-3.00$
--------
Regards,
Bill Page.
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer