diff options
Diffstat (limited to 'build')
| -rw-r--r-- | build/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/build/Makefile b/build/Makefile index fd06b6c80..17f6f786b 100644 --- a/build/Makefile +++ b/build/Makefile @@ -29,7 +29,8 @@ $(TARGETS): %: if [ "$$format" = html ]; then \ mkdir -p "$$arch_destination/$$destsuffix/images" ; \ mv ./$$destdir/html/images/* "$$arch_destination/$$destsuffix/images" ; \ - rmdir ./$$destdir/html/images ; \ + ls -la ./$$destdir/html/images; \ + rmdir ./$$destdir/html/images || true ; \ mv ./$$destdir/html/* "$$arch_destination/$$destsuffix" ; \ else \ # Do not fail because of missing PDF support for some languages \ |