From 83a646f2b362a3cff9032fb24e288e70bfc24aa9 Mon Sep 17 00:00:00 2001 From: Samuel Thibault Date: Sat, 18 Apr 2015 10:41:10 +0000 Subject: debug why jenkins fails to build manual --- build/Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'build') 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 \ -- cgit v1.2.3