docbuild errors out with "cannot copy static file FileExistsError"

[Dima Pasechnik]

observed with the latest beta on Linux and macOS:

...
[dochtml] [reference] valuations: 1 todos, 14 index, 0 citations, 13 modules
[dochtml] [reference] ... done (499 todos, 2531 index, 1644 citations,
2153 modules)
[dochtml] [reference] preparing documents... skipping loading of indexes... done
[dochtml] [reference] Merging js index files...
[dochtml] [reference] algebras: 4424 js index entries
[dochtml] [reference] arithgroup: 1204 js index entries
...

[dochtml] [reference] topology: 1937 js index entries
[dochtml] [reference] valuations: 973 js index entries
[dochtml] [reference] ... done (64387 js index entries)
[dochtml] [reference] copying static files... failed
[dochtml] [reference] WARNING: cannot copy static file
FileExistsError(17, 'File exists')
[dochtml] [reference] dumping search index in English (code: en)... done
[dochtml] [reference] The HTML pages are in
local/share/doc/sage/html/en/reference.
[dochtml] Error building the documentation.

make -j1

allows the docs to build (slowly)

[Kwankyu Lee]

Maybe related with 

https://trac.sagemath.org/ticket/31948

which you reviewed.

[Dima Pasechnik]

On Wed, Jul 21, 2021 at 1:28 AM Kwankyu Lee <ekwa...@gmail.com> wrote:
>
> Maybe related with
>
> https://trac.sagemath.org/ticket/31948
>
> which you reviewed.
>

probably; it's hard to test for race conditions.
I wrote there now:
"It's of course not totally surprising that several processes may try
to, say, create the same directory. Perhaps the relevant part of the
builder should be launched with this specific error being ignored? "
(https://trac.sagemath.org/ticket/31948#comment:85)

> --
> You received this message because you are subscribed to the Google Groups "sage-devel" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/e9de6e72-44d9-48ce-8942-141ed6a886f4n%40googlegroups.com.