DescriptionIssue 5380: Fix `make doc` with non-clean build directory
There was a possibility that the wrong PDF is output
if the build directory is not clean.
This commit makes `make doc` removes old files
in the destination directories `offline-root` and `online-root`.
Patch Set 1 #
Total comments: 2
Patch Set 2 : Use variable #MessagesTotal messages: 4
|