From 2785f0dd7a65c65cafa85e732ba359cfc9792b8b Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Wed, 18 Dec 2013 15:48:57 +0100
Subject: [PATCH] better Makefile entry for %-gallery

---
 Makefile.in | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Makefile.in b/Makefile.in
index fce148a86..9834762ca 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -451,7 +451,9 @@ gallery::
 	why3session html $$x; \
 	echo "exporting $$f"; \
 	mkdir -p $(GALLERYDIR)/$$f; \
-	cp examples/$$f.mlw examples/$$f/$$f.html $(GALLERYDIR)/$$f/; \
+	if test -f examples/$$f.mlw; then cp examples/$$f.mlw $(GALLERYDIR)/$$f/; fi; \
+	if test -f examples/$$f.why; then cp examples/$$f.why $(GALLERYDIR)/$$f/; fi; \
+	cp examples/$$f/$$f.html $(GALLERYDIR)/$$f/; \
 	rm -f $(GALLERYDIR)/$$f/$$f.zip; \
 	cd examples/; \
 	zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f/$$f.html  $$f
-- 
GitLab