Re: make --shuffle

[Bruno Haible]

Santiago Vila wrote:
> >> Note: The above error only happened once after several tries during the 
> >> last months,
> >> so it's random. On the other hand it has all the signs of being a Makefile 
> >> bug.

Since 'make' is known to deal with time stamps, I would
  1) make sure to use a local file system, not e.g. NFS or CIFS, for the build.
  2) make sure to build GNU make with the 'time' module from gnulib [1], as a
     workaround to [2].

Bruno

[1] https://www.gnu.org/software/gnulib/manual/html_node/time.html
[2] https://sourceware.org/bugzilla/show_bug.cgi?id=30200