> 'make doc' failed. > > It appears that under some conditions, we end up with a path > including '//'.
Multiple slashes in succession are completely harmless; they are simply equivalent to `/`. Doing a bit of an internet search it seems this is a bug in the `cp` implementation on macOS (as unbelievable it may be, given that `cp` is such a fundamental command that exists since decades): https://apple.stackexchange.com/questions/464706/why-do-i-get-bad-file-descriptor-when-copying-using-hardlink-flag Please read this and check whether you are affected by this problem. In case you can confirm the issue please try whether it works if you omit the `-l` option in all `cp` calls in my patch. Werner