diff options
| author | Samuel Thibault <sthibault@debian.org> | 2015-04-18 10:41:10 +0000 |
|---|---|---|
| committer | Samuel Thibault <sthibault@debian.org> | 2015-04-18 10:41:10 +0000 |
| commit | 83a646f2b362a3cff9032fb24e288e70bfc24aa9 (patch) | |
| tree | e554e178ddccb857d9c6dbfc733afcdc8691e08f /build | |
| parent | 9a411c4a17d9943f8f096e54352acd506e0eab04 (diff) | |
| download | installation-guide-83a646f2b362a3cff9032fb24e288e70bfc24aa9.zip | |
debug why jenkins fails to build manual
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 \ |