P.S., regarding the documentation of `.LOW_RESOLUTION_TIME' Here with GNU Make 3.81, I think you should not blame the cp command, but instead say "when using a mixture of filesystem types, or in some other situations, one might want to specify some files were made with low resolution timestamps..."
Indeed, for my situation all the files were low resolution (ext3), except this one on /tmp, where a .HIGH_RESOLUTION_TIME might have come in handy. _______________________________________________ Bug-make mailing list Bug-make@gnu.org http://lists.gnu.org/mailman/listinfo/bug-make