Re: GUB

[Masamichi Hosoda]

>> GUB worked for a long time, but we have a) an unsolved problem
>> building the pdfs of the english documentation of stable/2.20,
> 
> That sounds like more of a race condition to me, so it's likely
> unrelated to GUB but may be related to building in a separate directory
> or to cross-compilation.

I found a possibility that the wrong PDF is output
if the build directory is not clean.
This issue is unrelated to GUB.
With GUB, without GUB, it might happen in both.

You can reproduce by the following procedure without GUB.

```
$ git checkout release/2.19.82-1
$ ./autogen.sh --noconf
$ rm -fr build
$ mkdir build
$ mkdir -p out-www/offline-root/Documentation/
$ echo "wrong file" > out-www/offline-root/Documentation/notation.pdf
$ mkdir -p out-www/online-root/Documentation/
$ echo "wrong file" > out-www/online-root/Documentation/notation.pdf
$ ../configure
$ make -j 8
$ make -j 8 CPU_COUNT=8 WEB_TARGETS='offline online' LANGS='' doc
```

The result is as follows.

```
$ find . -name 'notation.pdf' -exec ls -lah {} \;
-rw-r--r-- 1 trueroad none 6.5M Jul 13 22:37 
./Documentation/out-www/notation.pdf
-rw-r--r-- 1 trueroad none 11 Jul 13 21:39 
./out-www/offline-root/Documentation/notation.pdf
-rw-r--r-- 1 trueroad none 11 Jul 13 21:39 
./out-www/online-root/Documentation/notation.pdf

$ cat out-www/offline-root/Documentation/notation.pdf
wrong file

$ cat out-www/online-root/Documentation/notation.pdf
wrong file

$
```

I'll create a patch which fixes this issue.