better Makefile entry for %-gallery

parent 467bef94
......@@ -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/$$; \
cd examples/; \
zip -r $(GALLERYDIR)/$$f/$$ $$f.mlw $$f/$$f.html $$f
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment