gallery regeneration: create also html reports

73425da5 · MARCHE Claude · 48d11435 · 73425da5
Commit 73425da5 authored Mar 25, 2013 by MARCHE Claude
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 2 deletions

Makefile.in Makefile.in +3 -2

No files found.
--- a/Makefile.in
+++ b/Makefile.in
@@ -429,12 +429,13 @@ gallery::
 	@for x in examples/*/why3session.xml ; do \
 	  d=`dirname $$x`; \
 	  f=`basename $$d`; \
+	  why3session html $$x; \
 	  echo "exporting $$f"; \
 	  mkdir -p $(GALLERYDIR)/$$f; \
-	  cp examples/$$f.mlw $(GALLERYDIR)/$$f/; \
+	  cp examples/$$f.mlw examples/$$f/$$f.html $(GALLERYDIR)/$$f/; \
 	  rm -f $(GALLERYDIR)/$$f/$$f.zip; \
 	  cd examples/; \
-	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f; \
+	  zip -r $(GALLERYDIR)/$$f/$$f.zip $$f.mlw $$f/$$f.html  $$f; \
 	  cd ..; \
 	done